# HG changeset patch
# User wenzelm
# Date 1703339525 -3600
# Node ID 7e57d2581ba1f7d087791da3d29cfbbb7f391569
# Parent  032a31db4c6f371befb8915fdfe32814b55e568e
minor performance tuning;

diff -r 032a31db4c6f -r 7e57d2581ba1 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Fri Dec 22 21:03:16 2023 +0100
+++ b/src/Pure/conjunction.ML	Sat Dec 23 14:52:05 2023 +0100
@@ -150,8 +150,10 @@
 val B = read_prop "B";
 
 fun comp_rule th rule =
-  Thm.adjust_maxidx_thm ~1 (th COMP
-    (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
+  let
+    val frees = Names.build (rule |> Thm.fold_terms {hyps = true} Names.add_free_names);
+    val idx = Thm.maxidx_of th + 1;
+  in Thm.adjust_maxidx_thm ~1 (th COMP (rule |> Thm.generalize (Names.empty, frees) idx)) end;
 
 in