src/Pure/Isar/runtime.ML

--- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 18:07:40 2011 +0200
@@ -61,7 +61,7 @@
       | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
       | flatten context exn =
           (case Par_Exn.dest exn of
-            SOME exns => map (pair context) exns
+            SOME exns => maps (flatten context) exns
           | NONE => [(context, Par_Exn.serial exn)]);
 
     fun exn_msgs (context, (i, exn)) =
@@ -98,7 +98,7 @@
             | _ => raised exn (General.exnMessage exn) []);
         in [(i, msg)] end)
       and sorted_msgs context exn =
-        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;