src/Pure/Isar/toplevel.ML
changeset 50917 9459f59cff09
parent 50739 5165d7e6d3b9
child 51216 e6e7685fc8f8
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:39:43 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:49:56 2013 +0100
     1.3 @@ -88,7 +88,6 @@
     1.4    val unknown_context: transition -> transition
     1.5    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     1.6    val status: transition -> Markup.T -> unit
     1.7 -  val error_msg: transition -> serial * string -> unit
     1.8    val add_hook: (transition -> state -> state -> unit) -> unit
     1.9    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    1.10    val command: transition -> state -> state
    1.11 @@ -596,9 +595,6 @@
    1.12  fun status tr m =
    1.13    setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
    1.14  
    1.15 -fun error_msg tr msg =
    1.16 -  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
    1.17 -
    1.18  
    1.19  (* post-transition hooks *)
    1.20