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