--- 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>