src/Pure/Thy/thy_read.ML
changeset 397 48cb3fa4bc59
parent 391 e960fe156cd8
child 412 216624270b80
--- 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;