# HG changeset patch
# User wenzelm
# Date 912520046 -3600
# Node ID c1f28f8ec72c8a0d8df5ea3105d3b3531712d909
# Parent  28b0a98918525d0678c890d80ede4f51c7aaf78f
excursion: ERROR_MESSAGE;
exn_message: ERROR;

diff -r 28b0a9891852 -r c1f28f8ec72c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Dec 01 14:46:58 1998 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Dec 01 14:47:26 1998 +0100
@@ -254,6 +254,7 @@
   | exn_message (BREAK _) = "Break."
   | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   | exn_message Interrupt = "Interrupt (exec)."
+  | exn_message ERROR = "ERROR."
   | exn_message (ERROR_MESSAGE msg) = msg
   | exn_message (THEORY (msg, _)) = msg
   | exn_message (ProofContext.CONTEXT (msg, _)) = msg
@@ -341,7 +342,7 @@
 fun excursion trs =
   (case excur trs (State []) of
     State [] => ()
-  | _ => error "Pending blocks at end of excursion");
+  | _ => raise ERROR_MESSAGE "Pending blocks at end of excursion");