# HG changeset patch
# User wenzelm
# Date 1701854977 -3600
# Node ID 42ca72f06632b2f6136dacb775220e20156c1947
# Parent  4e738f2a97a852af8c2dde6710479e510218c245
tuned;

diff -r 4e738f2a97a8 -r 42ca72f06632 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 05 22:04:01 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 10:29:37 2023 +0100
@@ -273,6 +273,9 @@
       | proof (ZClassP (T, c)) = ZClassP (typ T, c);
   in proof end;
 
+fun map_proof_types_same typ =
+  map_proof_same typ (subst_term_same typ Same.same);
+
 
 (* instantiation *)
 
@@ -524,7 +527,6 @@
           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
           | SOME w => ZTVar w));
-      val term = subst_term_same typ Same.same;
-    in Same.commit (map_proof_same typ term) prf end;
+    in Same.commit (map_proof_types_same typ) prf end;
 
 end;