Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/context_rules.ML
changeset 82873 e567fd948ff0
parent 82868 c2a88a1cd07d
child 82874 abfb6ed8ec21 
--- 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
isabelle