src/Pure/Isar/isar_cmd.ML
changeset 37949 48a874444164
parent 37870 dd9cfc512b7f
child 37952 f6c40213675b
--- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 23 18:42:46 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 24 12:14:53 2010 +0200
@@ -274,10 +274,9 @@
 (* init and exit *)
 
 fun init_theory (name, imports, uses) =
-  Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
-    (fn thy =>
-      if Thy_Info.check_known_thy (Context.theory_name thy)
-      then Thy_Info.end_theory thy else ());
+  Toplevel.init_theory name
+    (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
+    (Theory.end_theory #> tap Thy_Load.check_loaded #> Thy_Info.end_theory);
 
 val exit = Toplevel.keep (fn state =>
  (Context.set_thread_data (try Toplevel.generic_theory_of state);