tuned signature;

--- 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 *)
 

--- 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