diff -r 25669513fd4c -r 0966ac3f4a40 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Oct 02 14:22:36 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Oct 02 14:22:40 2008 +0200
@@ -963,7 +963,7 @@
         Exn.Result (SOME _) => goal_state
       | Exn.Result NONE => error (fail_msg (context_of goal_state))
       | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
-      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
+      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 
 in