Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed syntax of use_string
authorclasohm
Thu, 26 May 1994 13:45:43 +0200
changeset 397 48cb3fa4bc59
parent 396 18c9c28d0f7e
child 398 41f279b477e2
changed syntax of use_string
src/Pure/Thy/read.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_read.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/read.ML	Thu May 26 13:37:51 1994 +0200
+++ b/src/Pure/Thy/read.ML	Thu May 26 13:45:43 1994 +0200
@@ -259,8 +259,8 @@
          else (writeln ("Reading \"" ^ name ^ ".ML\"");
                use ml_file);
 
-         use_string ("store_theory " ^ quote thy_name ^ " " 
-                     ^ thy_name ^ ".thy");
+         use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name 
+                     ^ ".thy;"];
 
          (*Now set the correct info*)
          set_info (file_info thy_file) (file_info ml_file) thy_name;
--- a/src/Pure/Thy/thy_read.ML	Thu May 26 13:37:51 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML	Thu May 26 13:45:43 1994 +0200
@@ -262,8 +262,8 @@
          else (writeln ("Reading \"" ^ name ^ ".ML\"");
                use ml_file);
 
-         use_string ("store_theory " ^ quote thy_name ^ " " 
-                     ^ thy_name ^ ".thy");
+         use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name 
+                     ^ ".thy;"];
 
          (*Now set the correct info*)
          set_info (file_info thy_file) (file_info ml_file) thy_name;
isabelle