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*)

mercurial