src/Pure/Thy/thy_load.ML
changeset 37952 f6c40213675b
parent 37950 bc285d91041e
child 37977 3ceccd415145
--- 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 *)