diff -r 18c9c28d0f7e -r 48cb3fa4bc59 src/Pure/Thy/read.ML
--- 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;