# HG changeset patch
# User wenzelm
# Date 1717956281 -7200
# Node ID 9aa11b457c3613660764f9ae6e31a8f8418be01f
# Parent  718daea1cf99175d161b1fe5769decbcfaba1313
tuned: more direct Isabelle/ML;

diff -r 718daea1cf99 -r 9aa11b457c36 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Sun Jun 09 19:49:42 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Sun Jun 09 20:04:41 2024 +0200
@@ -137,10 +137,7 @@
       if is_none some_method_ref then ["  .."]
       else ["  by" ^ method_text]
       else print ctxt_print method_text clauses;
-    val message = Active.sendback_markup_command (cat_lines lines);
-  in
-    (state |> tap (fn _ => Output.information message))
-  end
+  in Output.information (Active.sendback_markup_command (cat_lines lines)) end;
 
 val sketch = print_proof_text_from_state print_sketch;
 
@@ -157,10 +154,10 @@
   end;
 
 fun sketch_cmd some_method_text =
-  Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)
+  Toplevel.keep_proof (fn state => sketch some_method_text (Toplevel.proof_of state));
 
 fun explore_cmd method_text =
-  Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of)
+  Toplevel.keep_proof (fn state => explore method_text (Toplevel.proof_of state));
 
 fun subgoals_cmd (modes, method_ref) =
   let
@@ -168,8 +165,9 @@
     val is_for = not (member (op =) modes "nofor")
     val is_sh = member (op =) modes "sh"
   in
-    Toplevel.keep_proof (K () o subgoals (is_prems, is_for, is_sh) method_ref o Toplevel.proof_of)
-  end
+    Toplevel.keep_proof (fn state =>
+      subgoals (is_prems, is_for, is_sh) method_ref (Toplevel.proof_of state))
+  end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>sketch\<close>