# HG changeset patch
# User wenzelm
# Date 1185903628 -7200
# Node ID 74926cdbf071136d345f7ec353051cf28a0803f2
# Parent  785c3cd7fcb5a93f09a28f59784ea916eccfbcc0
register_thy: more sanity checks;

diff -r 785c3cd7fcb5 -r 74926cdbf071 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);