# HG changeset patch
# User Simon Wimmer <wimmers@in.tum.de>
# Date 1710188436 -3600
# Node ID 54e9875e491f3644db9967e96fa25ddfe0e9aa1c
# Parent  8f0ff2847ba8ba26a855a0884bb11cb55bfcf8e3
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)

diff -r 8f0ff2847ba8 -r 54e9875e491f src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:31:18 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:20:36 2024 +0100
@@ -6,7 +6,7 @@
 
 theory Sketch_and_Explore
   imports Main \<comment> \<open>TODO: generalize existing sledgehammer functions to Pure\<close>
-  keywords "sketch" "nxsketch" "explore" :: diag
+  keywords "sketch" "explore" :: diag
 begin
 
 ML \<open>
@@ -60,10 +60,7 @@
     s
   end;
 
-fun print_nonext_sketch ctxt method_text clauses =
-  "proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"];
-
-fun print_next_skeleton ctxt indent keyword stmt =
+fun print_skeleton ctxt indent keyword stmt =
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
@@ -80,11 +77,8 @@
     s
   end;
 
-fun print_next_sketch ctxt method_text clauses =
-  "proof" ^ method_text :: separate "next" (map (print_next_skeleton ctxt 2 "show") clauses) @ ["qed"];
-
-fun print_sketch ctxt method_text [cl] = print_next_sketch ctxt method_text [cl]
-  | print_sketch ctxt method_text clauses = print_nonext_sketch ctxt method_text clauses;
+fun print_sketch ctxt method_text clauses =
+  "proof" ^ method_text :: separate "next" (map (print_skeleton ctxt 2 "show") clauses) @ ["qed"];
 
 fun print_exploration ctxt method_text [clause] =
     ["proof -", print_isar_skeleton ctxt 2 "have" clause,
@@ -130,16 +124,11 @@
 
 val sketch = print_proof_text_from_state print_sketch;
 
-val next_sketch = print_proof_text_from_state print_next_sketch;
-
 fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref);
 
 fun sketch_cmd some_method_text =
   Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)
 
-fun next_sketch_cmd some_method_text =
-  Toplevel.keep_proof (K () o next_sketch some_method_text o Toplevel.proof_of)
-
 fun explore_cmd method_text =
   Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of)
 
@@ -149,11 +138,6 @@
     (Scan.option (Scan.trace Method.parse) >> sketch_cmd);
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>nxsketch\<close>
-    "print sketch of Isar proof text after method application"
-    (Scan.option (Scan.trace Method.parse) >> next_sketch_cmd);
-
-val _ =
   Outer_Syntax.command \<^command_keyword>\<open>explore\<close>
     "explore proof obligations after method application as Isar proof text"
     (Scan.trace Method.parse >> explore_cmd);