# HG changeset patch
# User wenzelm
# Date 1216058231 -7200
# Node ID e0cd0396945aa8ae4da37635405a50ad8979e9ef
# Parent  9109f0d8a565a383f7b4b4cba44ce4031f4a3c67
commit_exit: proper error;

diff -r 9109f0d8a565 -r e0cd0396945a src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Mon Jul 14 19:57:09 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Mon Jul 14 19:57:11 2008 +0200
@@ -174,8 +174,8 @@
     (case (Toplevel.is_toplevel st, prev_command id) of
       (true, SOME prev) =>
         (case Toplevel.transition true Toplevel.commit_exit (#1 (the_result prev)) of
-          SOME (_, SOME (exn, msg)) => raise Exn.EXCEPTIONS ([exn], msg)
-        | _ => ())
+          SOME (_, SOME err) => error (Toplevel.exn_message (Toplevel.EXCURSION_FAIL err))
+        | _ => init_point ())
     | _ => error "Expected to find finished theory")
   end;