# HG changeset patch
# User wenzelm
# Date 1737582639 -3600
# Node ID 658f3237eaddbb2f14474bdcae964fad89069a23
# Parent  33616e13e17273ab9bfec9db0fd273ad8fededf9
minor performance tuning: omit redundant inst_cterm;

diff -r 33616e13e172 -r 658f3237eadd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Jan 22 22:37:38 2025 +0100
+++ b/src/Pure/more_thm.ML	Wed Jan 22 22:50:39 2025 +0100
@@ -408,24 +408,21 @@
   if TFrees.is_empty instT andalso Frees.is_empty inst then th
   else
     let
-      val idx = Thm.maxidx_of th + 1;
-      fun index ((a, A), b) = (((a, idx), A), b);
-      val insts =
-        (TVars.build (TFrees.fold (TVars.add o index) instT),
-         Vars.build (Frees.fold (Vars.add o index) inst));
       val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
       val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
 
+      val idx = Thm.maxidx_of th + 1;
+      fun index ((a, A), b) = (((a, idx), A), b);
+      val instT' = TVars.build (TFrees.fold (TVars.add o index) instT);
+      val inst' = Vars.build (Frees.fold (Vars.add o index) inst);
+
       val hyps = Thm.chyps_of th;
-      val inst_cterm =
-        Thm.generalize_cterm (tfrees, frees) idx #>
-        Thm.instantiate_cterm insts;
     in
       th
       |> fold_rev Thm.implies_intr hyps
       |> Thm.generalize (tfrees, frees) idx
-      |> Thm.instantiate insts
-      |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+      |> Thm.instantiate (instT', inst')
+      |> assume_prems (length hyps)
     end;