# HG changeset patch
# User wenzelm
# Date 1737126215 -3600
# Node ID 3ba99477b893323a71b93dcf35c4a2f242cf2a58
# Parent  4af2e864c26c262cab0a8300dde13cb1868b8ed0
minor performance tuning;

diff -r 4af2e864c26c -r 3ba99477b893 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 15:39:40 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 16:03:35 2025 +0100
@@ -151,10 +151,13 @@
 
 fun freezeT thy th =
   let
-    val tvars = Term.add_tvars (Thm.prop_of th) []
-    val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
+    fun add (v as ((a, _), S)) tvars =
+      if TVars.defined tvars v then tvars
+      else TVars.add (v, Thm.global_ctyp_of thy (TFree (a, S))) tvars
+    val tyinst =
+      TVars.build (Thm.prop_of th |> (fold_types o fold_atyps) (fn TVar v => add v | _ => I))
   in
-    Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) th
+    Thm.instantiate (tyinst, Vars.empty) th
   end
 
 fun def' c rhs thy =