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