--- 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