# HG changeset patch
# User wenzelm
# Date 1752571591 -7200
# Node ID e567fd948ff0803793ed67705ed8ad267fdc1147
# Parent  898d3860a2042945b49e2265643b5a174b617397
clarified signature;

diff -r 898d3860a204 -r e567fd948ff0 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 15 11:22:02 2025 +0200
+++ b/src/Provers/classical.ML	Tue Jul 15 11:26:31 2025 +0200
@@ -353,7 +353,7 @@
   else if kind = Bires.elim_bang_kind orelse kind = Bires.dest_bang_kind then
     let
       val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
-      val elim = if Bires.kind_make_elim kind then Tactic.make_elim th else th;
+      val elim = Bires.kind_make_elim kind th;
     in make_info1 (no_swapped_rl (classical_rule ctxt (flat_rule ctxt elim))) elim end
   else if kind = Bires.intro_kind then
     let
@@ -363,7 +363,7 @@
   else if kind = Bires.elim_kind orelse kind = Bires.dest_kind then
     let
       val _ = Thm.no_prems th andalso err_thm_illformed ctxt kind th;
-      val elim = if Bires.kind_make_elim kind then Tactic.make_elim th else th;
+      val elim = Bires.kind_make_elim kind th;
       val th' = classical_rule ctxt (flat_rule ctxt elim);
       val dup_th' = dup_elim ctxt th' handle THM _ => err_thm_illformed ctxt kind th;
     in make_info (no_swapped_rl th') (no_swapped_rl dup_th') elim end
diff -r 898d3860a204 -r e567fd948ff0 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Jul 15 11:22:02 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Jul 15 11:26:31 2025 +0200
@@ -68,7 +68,7 @@
 fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) =
   let
     val th' = Thm.trim_context th;
-    val th'' = if Bires.kind_make_elim kind then Thm.trim_context (Tactic.make_elim th) else th';
+    val th'' = Thm.trim_context (Bires.kind_make_elim kind th);
     val decl' = init_decl kind opt_weight th'';
   in
     (case Bires.extend_decls (th', decl') decls of
diff -r 898d3860a204 -r e567fd948ff0 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Tue Jul 15 11:22:02 2025 +0200
+++ b/src/Pure/bires.ML	Tue Jul 15 11:26:31 2025 +0200
@@ -35,7 +35,7 @@
   val kind_extra: kind -> bool
   val kind_index: kind -> int
   val kind_is_elim: kind -> bool
-  val kind_make_elim: kind -> bool
+  val kind_make_elim: kind -> thm -> thm
   val kind_name: kind -> string
   val kind_domain: kind list
   val kind_values: 'a -> 'a list
@@ -146,7 +146,7 @@
 fun kind_extra (Kind {index, ...}) = index = 2;
 fun kind_index (Kind {index, ...}) = index;
 fun kind_is_elim (Kind {is_elim, ...}) = is_elim;
-fun kind_make_elim (Kind {make_elim, ...}) = make_elim;
+fun kind_make_elim (Kind {make_elim, ...}) = make_elim ? Tactic.make_elim;
 
 fun kind_name (Kind {is_elim, make_elim, ...}) =
   if is_elim andalso make_elim then "destruction rule"