# HG changeset patch
# User wenzelm
# Date 1737126828 -3600
# Node ID 81f3adce1eda4160a4413c25b8cc24bed2de1261
# Parent  3ba99477b893323a71b93dcf35c4a2f242cf2a58
minor performance tuning: more elementary operations;

diff -r 3ba99477b893 -r 81f3adce1eda src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 16:03:35 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 16:13:48 2025 +0100
@@ -160,6 +160,18 @@
     Thm.instantiate (tyinst, Vars.empty) th
   end
 
+fun freeze thy = freezeT thy #> (fn th =>
+  let
+    val vars = Vars.build (th |> Thm.add_vars)
+    val inst = vars |> Vars.map (fn _ => fn v =>
+      let
+        val Var ((x, _), _) = Thm.term_of v
+        val ty = Thm.ctyp_of_cterm v
+      in Thm.free (x, ty) end)
+  in
+    Thm.instantiate (TVars.empty, inst) th
+  end)
+
 fun def' c rhs thy =
   let
     val b = Binding.name c
@@ -375,11 +387,9 @@
       | process (#"M", [s]) = (fn state =>
           let
             val thy = get_theory state
-            val ctxt = Proof_Context.init_global thy
-            val th = freezeT thy (Global_Theory.get_thm thy s)
-            val ((_, [th']), _) = Variable.import true [th] ctxt
+            val th = freeze thy (Global_Theory.get_thm thy s)
           in
-            set_thm th' state
+            set_thm th state
           end)
       | process (#"Q", l) = (fn state =>
           let