src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Wed Apr 22 18:43:33 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 22 19:48:32 2015 +0200
@@ -40,7 +40,6 @@
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
-  val imperative: (unit -> unit) -> transition -> transition
   val ignored: Position.T -> transition
   val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
@@ -345,13 +344,12 @@
 fun transaction f = present_transaction f (K ());
 
 fun keep f = add_trans (Keep (fn _ => f));
-fun imperative f = keep (fn _ => f ());
 
-fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
 fun is_ignored tr = name_of tr = "<ignored>";
 
 fun malformed pos msg =
-  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
+  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
 
 
 (* theory transitions *)