register_thy: more sanity checks;
authorwenzelm
Tue, 31 Jul 2007 19:40:28 +0200
changeset 24096 74926cdbf071
parent 24095 785c3cd7fcb5
child 24097 86734ba03ca2
register_thy: more sanity checks;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 31 19:40:26 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 31 19:40:28 2007 +0200
@@ -527,6 +527,8 @@
   let
     val _ = priority ("Registering theory " ^ quote name);
     val _ = get_theory name;
+    val _ = map get_theory (get_parents name);
+    val _ = check_unfinished error name;
     val _ = touch_thy name;
     val files = check_files name;
     val master = #master (ThyLoad.deps_thy Path.current name false);