improved cycle error;
authorwenzelm
Thu Sep 23 18:42:28 1999 +0200 (1999-09-23 ago)
changeset 758959663b367833
parent 7588 26384af93359
child 7590 76c9e71d491a
improved cycle error;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Sep 23 18:39:05 1999 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Sep 23 18:42:28 1999 +0200
     1.3 @@ -250,7 +250,6 @@
     1.4  
     1.5  fun load_thy ml time initiators dir name parents =
     1.6    let
     1.7 -    val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
     1.8      val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
     1.9  
    1.10      val _ = touch_thy name;
    1.11 @@ -299,6 +298,7 @@
    1.12      val path = Path.expand (Path.unpack str);
    1.13      val name = Path.pack (Path.base path);
    1.14    in
    1.15 +    if name mem_string initiators then error (cycle_msg name initiators) else ();
    1.16      if name mem_string visited then (visited, (true, name))
    1.17      else
    1.18        let