# HG changeset patch
# User wenzelm
# Date 1752486374 -7200
# Node ID 639ceaf8eb0d53d7e9e0c509a7bf44eafcb20682
# Parent  2703f19d323e08e92c787e060fc9c8e11596c88d
tuned;

diff -r 2703f19d323e -r 639ceaf8eb0d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Jul 14 11:18:10 2025 +0200
+++ b/src/Provers/classical.ML	Mon Jul 14 11:46:14 2025 +0200
@@ -349,10 +349,31 @@
 fun trim_context_info {rl, dup_rl, plain} : info =
   {rl = trim_context_rl rl, dup_rl = trim_context_rl dup_rl, plain = Thm.trim_context plain};
 
-fun extend_rules ctxt kind opt_weight (th, info) cs =
+fun ext_info ctxt kind th =
+  if kind = Bires.intro_bang_kind then
+    make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th
+  else if kind = Bires.elim_bang_kind then
+    let val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th
+    in make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th end
+  else if kind = Bires.intro_kind then
+    let
+      val th' = flat_rule ctxt th;
+      val dup_th' = dup_intr th' handle THM _ => err_thm_illformed ctxt kind th;
+    in make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th end
+  else if kind = Bires.elim_kind then
+    let
+      val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
+      val th' = classical_rule ctxt (flat_rule ctxt th);
+      val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th th;
+    in make_info (no_swapped_rl th') (no_swapped_rl dup_th') th end
+  else raise Fail "Bad rule kind";
+
+in
+
+fun extend_rules ctxt kind opt_weight th cs =
   let
     val th' = Thm.trim_context th;
-    val decl' = init_decl kind opt_weight (trim_context_info info);
+    val decl' = init_decl kind opt_weight (trim_context_info (ext_info ctxt kind th));
     val CS {decls, swrappers, uwrappers, safe0_netpair, safep_netpair,
       unsafe_netpair, dup_netpair, extra_netpair} = cs;
   in
@@ -377,8 +398,6 @@
         end)
   end;
 
-in
-
 fun merge_cs (cs, cs2) =
   if pointer_eq (cs, cs2) then cs
   else
@@ -403,38 +422,6 @@
         extra_netpair = extra_netpair'}
     end;
 
-fun addSI w ctxt th cs =
-  extend_rules ctxt Bires.intro_bang_kind w
-    (th, make_info1 (maybe_swapped_rl (flat_rule ctxt th)) th) cs;
-
-fun addSE w ctxt th cs =
-  let
-    val kind = Bires.elim_bang_kind;
-    val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
-    val info = make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt th))) th;
-  in extend_rules ctxt kind w (th, info) cs end;
-
-fun addSD w ctxt th = addSE w ctxt (make_elim ctxt th);
-
-fun addI w ctxt th cs =
-  let
-    val kind = Bires.intro_kind;
-    val th' = flat_rule ctxt th;
-    val dup_th' = dup_intr th' handle THM _ => err_thm_illformed ctxt kind th;
-    val info = make_info (maybe_swapped_rl th') (maybe_swapped_rl dup_th') th;
-  in extend_rules ctxt kind w (th, info) cs end;
-
-fun addE w ctxt th cs =
-  let
-    val kind = Bires.elim_kind;
-    val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
-    val th' = classical_rule ctxt (flat_rule ctxt th);
-    val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th th;
-    val info = make_info (no_swapped_rl th') (no_swapped_rl dup_th') th;
-  in extend_rules ctxt kind w (th, info) cs end;
-
-fun addD w ctxt th = addE w ctxt (make_elim ctxt th);
-
 end;
 
 
@@ -503,17 +490,19 @@
 fun put_claset cs = map_claset (K cs);
 
 
-(* old-style declarations *)
+(* old-style ML declarations *)
 
-fun decl f (ctxt, ths) = map_claset (fold_rev (f ctxt) ths) ctxt;
+fun ml_decl kind view (ctxt, ths) =
+  map_claset (fold_rev (extend_rules ctxt kind NONE o view ctxt) ths) ctxt;
 
-val op addSIs = decl (addSI NONE);
-val op addSEs = decl (addSE NONE);
-val op addSDs = decl (addSD NONE);
-val op addIs = decl (addI NONE);
-val op addEs = decl (addE NONE);
-val op addDs = decl (addD NONE);
-val op delrules = decl delrule;
+val op addSIs = ml_decl Bires.intro_bang_kind (K I);
+val op addSEs = ml_decl Bires.elim_bang_kind (K I);
+val op addSDs = ml_decl Bires.elim_bang_kind make_elim;
+val op addIs = ml_decl Bires.intro_kind (K I);
+val op addEs = ml_decl Bires.elim_kind (K I);
+val op addDs = ml_decl Bires.elim_kind make_elim;
+
+fun ctxt delrules ths = map_claset (fold_rev (delrule ctxt) ths) ctxt;
 
 
 
@@ -744,16 +733,17 @@
 
 (* declarations *)
 
-fun attrib f =
+fun attrib kind view w =
   Thm.declaration_attribute (fn th => fn context =>
-    map_cs (f (Context.proof_of context) th) context);
+    let val ctxt = Context.proof_of context
+    in map_cs (extend_rules ctxt kind w (view ctxt th)) context end);
 
-val safe_elim = attrib o addSE;
-val safe_intro = attrib o addSI;
-val safe_dest = attrib o addSD;
-val unsafe_elim = attrib o addE;
-val unsafe_intro = attrib o addI;
-val unsafe_dest = attrib o addD;
+val safe_intro = attrib Bires.intro_bang_kind (K I);
+val safe_elim = attrib Bires.elim_bang_kind (K I);
+val safe_dest = attrib Bires.elim_bang_kind make_elim;
+val unsafe_intro = attrib Bires.intro_kind (K I);
+val unsafe_elim = attrib Bires.elim_kind (K I);
+val unsafe_dest = attrib Bires.elim_kind make_elim;
 
 val rule_del =
   Thm.declaration_attribute (fn th => fn context =>