tuned source structure;

--- a/src/Provers/classical.ML	Fri Jul 11 23:36:13 2025 +0200
+++ b/src/Provers/classical.ML	Fri Jul 11 23:44:43 2025 +0200
@@ -37,7 +37,6 @@
 sig
   type wrapper = (int -> tactic) -> int -> tactic
   type claset
-  val print_claset: Proof.context -> unit
   val addDs: Proof.context * thm list -> Proof.context
   val addEs: Proof.context * thm list -> Proof.context
   val addIs: Proof.context * thm list -> Proof.context
@@ -93,6 +92,8 @@
   val inst_step_tac: Proof.context -> int -> tactic
   val inst0_step_tac: Proof.context -> int -> tactic
   val instp_step_tac: Proof.context -> int -> tactic
+
+  val print_claset: Proof.context -> unit
 end;
 
 signature CLASSICAL =
@@ -262,7 +263,7 @@
 fun rep_cs (CS args) = args;
 
 
-(* insert / delete rules in underlying netpairs *)
+(* netpair primitives to insert / delete rules *)
 
 fun insert_brl i brl =
   Bires.insert_tagged_rule ({weight = Bires.subgoals_of brl, index = i}, brl);
@@ -281,10 +282,13 @@
 fun delete_plain_rule ({tag = {index, ...}, info = {plain = th, ...}, ...}: decl) =
   Bires.delete_tagged_rule (index, th);
 
-fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
+
+(* erros and warnings *)
+
+fun err_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
 
 fun make_elim ctxt th =
-  if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th
+  if Thm.no_prems th then err_thm ctxt "Ill-formed destruction rule" th
   else Tactic.make_elim th;
 
 fun init_decl kind opt_weight info : decl =
@@ -311,23 +315,6 @@
   end;
 
 
-(* update wrappers *)
-
-fun map_swrappers f
-  (CS {decls, swrappers, uwrappers,
-    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  CS {decls = decls, swrappers = f swrappers, uwrappers = uwrappers,
-    safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
-    unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair};
-
-fun map_uwrappers f
-  (CS {decls, swrappers, uwrappers,
-    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
-  CS {decls = decls, swrappers = swrappers, uwrappers = f uwrappers,
-    safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
-    unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair};
-
-
 (* extend and merge rules *)
 
 local
@@ -418,7 +405,7 @@
     (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs;
 
 fun addSE w ctxt th cs =
-  if Thm.no_prems th then bad_thm ctxt "Ill-formed elimination rule" th
+  if Thm.no_prems th then err_thm ctxt "Ill-formed elimination rule" th
   else
     let val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th
     in extend_rules ctxt Bires.elim_bang_kind w (th, info) cs end;
@@ -428,15 +415,15 @@
 fun addI w ctxt th cs =
   let
     val th' = flat_rule ctxt th;
-    val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th;
+    val dup_th' = dup_intr th' handle THM _ => err_thm ctxt "Ill-formed introduction rule" th;
     val info = make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th;
   in extend_rules ctxt Bires.intro_kind w (th, info) cs end;
 
 fun addE w ctxt th cs =
   let
-    val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+    val _ = Thm.no_prems th andalso err_thm ctxt "Ill-formed elimination rule" th;
     val th' = classical_rule ctxt (flat_rule ctxt th);
-    val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
+    val dup_th' = dup_elim ctxt th' handle THM _ => err_thm ctxt "Ill-formed elimination rule" th;
     val info = make_info (no_swapped_rl th') (no_swapped_rl dup_th') th;
   in extend_rules ctxt Bires.elim_kind w (th, info) cs end;
 
@@ -509,17 +496,6 @@
 fun map_claset f = Context.proof_map (map_cs f);
 fun put_claset cs = map_claset (K cs);
 
-fun print_claset ctxt =
-  let
-    val {decls, swrappers, uwrappers, ...} = rep_claset_of ctxt;
-    val prt_rules =
-      Bires.pretty_decls ctxt
-        [Bires.intro_bang_kind, Bires.intro_kind, Bires.elim_bang_kind, Bires.elim_kind] decls;
-    val prt_wrappers =
-     [Pretty.strs ("safe wrappers:" :: map #1 swrappers),
-      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)];
-  in Pretty.writeln (Pretty.chunks (prt_rules @ prt_wrappers)) end;
-
 
 (* old-style declarations *)
 
@@ -537,6 +513,20 @@
 
 (** Modifying the wrapper tacticals **)
 
+fun map_swrappers f
+  (CS {decls, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  CS {decls = decls, swrappers = f swrappers, uwrappers = uwrappers,
+    safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
+    unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair};
+
+fun map_uwrappers f
+  (CS {decls, swrappers, uwrappers,
+    safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
+  CS {decls = decls, swrappers = swrappers, uwrappers = f uwrappers,
+    safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
+    unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair};
+
 fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
 fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
 
@@ -868,6 +858,17 @@
 
 (** outer syntax commands **)
 
+fun print_claset ctxt =
+  let
+    val {decls, swrappers, uwrappers, ...} = rep_claset_of ctxt;
+    val prt_rules =
+      Bires.pretty_decls ctxt
+        [Bires.intro_bang_kind, Bires.intro_kind, Bires.elim_bang_kind, Bires.elim_kind] decls;
+    val prt_wrappers =
+     [Pretty.strs ("safe wrappers:" :: map #1 swrappers),
+      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)];
+  in Pretty.writeln (Pretty.chunks (prt_rules @ prt_wrappers)) end;
+
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_claset\<close> "print context of Classical Reasoner"
     (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of)));