# HG changeset patch
# User wenzelm
# Date 1701810241 -3600
# Node ID 4e738f2a97a852af8c2dde6710479e510218c245
# Parent  bbef5d3ed56b24a6a5270287fb9aec5838081236
minor performance tuning;

diff -r bbef5d3ed56b -r 4e738f2a97a8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Dec 05 21:31:28 2023 +0100
+++ b/src/Pure/proofterm.ML	Tue Dec 05 22:04:01 2023 +0100
@@ -933,13 +933,18 @@
 (* varify *)
 
 fun varifyT_proof names prf =
-  let
-    val tab = TFrees.make names;
-    fun varify v =
-      (case TFrees.lookup tab v of
-        NONE => TFree v
-      | SOME w => TVar w);
-  in map_proof_terms (map_types (map_type_tfree varify)) (map_type_tfree varify) prf end;
+  if null names then prf
+  else
+    let
+      val tab = TFrees.make names;
+      val typ =
+        Term_Subst.map_atypsT_same
+          (fn TFree v =>
+              (case TFrees.lookup tab v of
+                NONE => raise Same.SAME
+              | SOME w => TVar w)
+            | _ => raise Same.SAME);
+    in Same.commit (map_proof_types_same typ) prf end;
 
 
 local