src/Pure/Isar/toplevel.ML
changeset 60189 0d3a62127057
parent 60099 d20ca79d50e4
child 60190 906de96ba68a
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 22 18:43:33 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 22 19:48:32 2015 +0200
     1.3 @@ -40,7 +40,6 @@
     1.4    val exit: transition -> transition
     1.5    val keep: (state -> unit) -> transition -> transition
     1.6    val keep': (bool -> state -> unit) -> transition -> transition
     1.7 -  val imperative: (unit -> unit) -> transition -> transition
     1.8    val ignored: Position.T -> transition
     1.9    val is_ignored: transition -> bool
    1.10    val malformed: Position.T -> string -> transition
    1.11 @@ -345,13 +344,12 @@
    1.12  fun transaction f = present_transaction f (K ());
    1.13  
    1.14  fun keep f = add_trans (Keep (fn _ => f));
    1.15 -fun imperative f = keep (fn _ => f ());
    1.16  
    1.17 -fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.18 +fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
    1.19  fun is_ignored tr = name_of tr = "<ignored>";
    1.20  
    1.21  fun malformed pos msg =
    1.22 -  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.23 +  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
    1.24  
    1.25  
    1.26  (* theory transitions *)