# HG changeset patch
# User wenzelm
# Date 1358369396 -3600
# Node ID 9459f59cff0941bda98790ff3ca9afae392dc07b
# Parent  fd902b616b4869824c11f6cd7b825f2c590a2593
tuned signature;

diff -r fd902b616b48 -r 9459f59cff09 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:39:43 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:49:56 2013 +0100
@@ -88,7 +88,6 @@
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
-  val error_msg: transition -> serial * string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
@@ -596,9 +595,6 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
 
-fun error_msg tr msg =
-  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
-
 
 (* post-transition hooks *)
 
diff -r fd902b616b48 -r 9459f59cff09 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Jan 16 21:39:43 2013 +0100
+++ b/src/Pure/System/isar.ML	Wed Jan 16 21:49:56 2013 +0100
@@ -96,7 +96,8 @@
     NONE => false
   | SOME (_, SOME exn_info) =>
      (set_exn (SOME exn_info);
-      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+      Toplevel.setmp_thread_position tr
+        Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
       true)
   | SOME (st', NONE) =>
       let