changeset
merged
Mon, 01 Apr 2019 23:51:35 +0200
- author
- wenzelm
- date
- Mon, 01 Apr 2019 23:51:35 +0200
- changeset 10275
- 7c585d0056e3
- parent 10273
- 0179ae771698 (current diff)
- parent 10274
- ceec86258d3f (diff)
- child 10276
- 1be13d9bf1cd
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*)
