improved cycle error;
authorwenzelm
Thu, 23 Sep 1999 18:42:28 +0200
changeset 7589 59663b367833
parent 7588 26384af93359
child 7590 76c9e71d491a
improved cycle error;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Sep 23 18:39:05 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Sep 23 18:42:28 1999 +0200
@@ -250,7 +250,6 @@
 
 fun load_thy ml time initiators dir name parents =
   let
-    val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
     val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
 
     val _ = touch_thy name;
@@ -299,6 +298,7 @@
     val path = Path.expand (Path.unpack str);
     val name = Path.pack (Path.base path);
   in
+    if name mem_string initiators then error (cycle_msg name initiators) else ();
     if name mem_string visited then (visited, (true, name))
     else
       let