Mon, 01 Apr 2019 23:51:35 +0200
merged
--- a/thys/Buchi_Complementation/Complementation_Build.thy Mon Apr 01 21:21:14 2019 +0100 +++ b/thys/Buchi_Complementation/Complementation_Build.thy Mon Apr 01 23:51:35 2019 +0200 @@ -38,7 +38,7 @@ val _ = if compile_rc = 0 then Export.export_executable_file thy - (Path.binding_map Path.exe \<^path_binding>\<open>code/Complementation\<close>) exe + (Path.map_binding Path.exe \<^path_binding>\<open>code/Complementation\<close>) exe else error "Compilation failed"; (*test*)
--- a/thys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy Mon Apr 01 21:21:14 2019 +0100 +++ b/thys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy Mon Apr 01 23:51:35 2019 +0200 @@ -35,7 +35,7 @@ val () = if compile_rc = 0 then Export.export_executable_file thy - (Path.binding_map Path.exe \<^path_binding>\<open>code/generated/hlde\<close>) exe + (Path.map_binding Path.exe \<^path_binding>\<open>code/generated/hlde\<close>) exe else error "Compilation failed"; (*test*)