# HG changeset patch
# User clasohm
# Date 826117844 -3600
# Node ID 4ee99a973be4fa512dd1048bdfab0c48d04f4642
# Parent  4eb4a9c7d73653d66443499526f69f3bf15464e7
moved part of delete_thms into init_thyinfo

diff -r 4eb4a9c7d736 -r 4ee99a973be4 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Mar 06 13:57:07 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Wed Mar 06 14:10:44 1996 +0100
@@ -356,11 +356,7 @@
                    thy_time = thy_time, ml_time = ml_time,
                    theory = theory, thms = Symtab.null,
                    methods = methods, data = data}
-      | None => ThyInfo {path = "", children = [], parents = [],
-                         thy_time = None, ml_time = None,
-                         theory = None, thms = Symtab.null,
-                         methods = Symtab.null,
-                         data = (Symtab.null, Symtab.null)};
+      | None => error ("Theory " ^ tname ^ " not stored by loader");
 
     val ThyInfo {theory, ...} = tinfo;
   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
@@ -694,7 +690,18 @@
  
          robust_seq add_to_parents new_parents
       end
-      end
+      end;
+
+    (*Make sure that loaded_thys contains an entry for tname*)
+    fun init_thyinfo () =
+    let val tinfo = ThyInfo {path = "", children = [], parents = [],
+                             thy_time = None, ml_time = None,
+                             theory = None, thms = Symtab.null,
+                             methods = Symtab.null,
+                             data = (Symtab.null, Symtab.null)};
+    in if is_some (get_thyinfo tname) then ()
+       else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
+    end;
   in if thy_uptodate andalso ml_uptodate then ()
      else
       (if thy_file = "" then ()
@@ -704,6 +711,7 @@
        else
          (writeln ("Reading \"" ^ name ^ ".thy\"");
 
+          init_thyinfo ();
           delete_thms tname;
           read_thy tname thy_file;
           use (out_name tname);