--- a/src/Pure/Isar/isar_cmd.ML Sat Jul 24 21:40:48 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Jul 25 12:57:29 2010 +0200
@@ -276,7 +276,7 @@
fun init_theory (name, imports, uses) =
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);
+ (Theory.end_theory #> Thy_Info.end_theory);
val exit = Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);