# HG changeset patch
# User wenzelm
# Date 1429724912 -7200
# Node ID 0d3a621270579e2c76b2f7e508e84a6e7b7aaee2
# Parent  b8b7006a64ef81c03020e39cc2d37a4bb416eb29
tuned signature;

diff -r b8b7006a64ef -r 0d3a62127057 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 22 18:43:33 2015 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 22 19:48:32 2015 +0200
@@ -42,7 +42,7 @@
 ML \<open>
   Outer_Syntax.command @{command_keyword cartouche} ""
     (Parse.cartouche >> (fn s =>
-      Toplevel.imperative (fn () => writeln s)))
+      Toplevel.keep (fn _ => writeln s)))
 \<close>
 
 cartouche \<open>abc\<close>
diff -r b8b7006a64ef -r 0d3a62127057 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 22 18:43:33 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 22 19:48:32 2015 +0200
@@ -854,13 +854,13 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword welcome} "print welcome message"
-    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
+    (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
 
 val _ =
   Outer_Syntax.command @{command_keyword display_drafts}
     "display raw source files with symbols"
     (Scan.repeat1 Parse.path >> (fn names =>
-      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
+      Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
 
 
 
diff -r b8b7006a64ef -r 0d3a62127057 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 *)
diff -r b8b7006a64ef -r 0d3a62127057 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed Apr 22 18:43:33 2015 +0200
+++ b/src/Pure/pure_syn.ML	Wed Apr 22 19:48:32 2015 +0200
@@ -43,7 +43,7 @@
 
 val _ =
   Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
-    (Parse.document_source >> K (Toplevel.imperative I));
+    (Parse.document_source >> K (Toplevel.keep (fn _ => ())));
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"