# HG changeset patch
# User wenzelm
# Date 1280055449 -7200
# Node ID f6c40213675b2ca90f04c9031d672118c1c760e5
# Parent  4e2aaf080572cde76823066e4b7ae675c8461367
Thy_Load.check_loaded via Theory.at_end;

diff -r 4e2aaf080572 -r f6c40213675b src/Pure/Isar/isar_cmd.ML
--- 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);
diff -r 4e2aaf080572 -r f6c40213675b src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Jul 24 21:40:48 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Jul 25 12:57:29 2010 +0200
@@ -27,7 +27,6 @@
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
   val loaded_files: theory -> Path.T list
-  val check_loaded: theory -> unit
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
@@ -178,6 +177,8 @@
       | SOME path_info' => eq_snd (op =) (path_info, path_info'));
   in can check_loaded thy andalso forall current provided end;
 
+val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
+
 
 (* provide files *)