# HG changeset patch
# User wenzelm
# Date 1262646269 -3600
# Node ID 2524c1bbd087f47c9543760806b8db092a92c98f
# Parent  2ba492b8b6e89e961754d950645b081cc926ff9f
kill failed theories in reverse order -- avoids cascaded warnings;

diff -r 2ba492b8b6e8 -r 2524c1bbd087 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jan 04 23:20:35 2010 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Jan 05 00:04:29 2010 +0100
@@ -389,14 +389,16 @@
 
     val futures = fold fork tasks Symtab.empty;
 
-    val exns = tasks |> maps (fn (name, _) =>
+    val failed = tasks |> maps (fn (name, _) =>
       let
         val after_load = Future.join (the (Symtab.lookup futures name));
         val _ = join_thy name;
         val _ = after_load ();
-      in [] end handle exn => (kill_thy name; [exn]));
+      in [] end handle exn => [(name, exn)]) |> rev;
 
-  in ignore (Exn.release_all (map Exn.Exn (rev exns))) end) ();
+    val _ = List.app (kill_thy o #1) failed;
+    val _ = Exn.release_all (map (Exn.Exn o #2) failed);
+  in () end) ();
 
 fun schedule_seq tasks =
   Graph.topological_order tasks