# HG changeset patch
# User wenzelm
# Date 1703009889 -3600
# Node ID dc6b58da806ea67e17dfbc44ce435ed360eea68e
# Parent  cf8ccfec5059f1a32d0af928b051af312d040914
omit unclear / inaccurate renaming;

diff -r cf8ccfec5059 -r dc6b58da806e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 19 18:03:25 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 19 19:18:09 2023 +0100
@@ -2255,19 +2255,6 @@
     if Symtab.forall (op =) vars andalso Symtab.forall (op =) bounds then NONE
     else
       let
-        fun zterm (ZVar ((x, i), T)) =
-              if i >= 0 then
-                let val y = perhaps (Symtab.lookup vars) x
-                in if x = y then raise Same.SAME else ZVar ((y, i), T) end
-              else raise Same.SAME
-          | zterm (ZAbs (x, T, t)) =
-              let val y = perhaps (Symtab.lookup bounds) x
-              in if x = y then ZAbs (x, T, zterm t) else ZAbs (y, T, Same.commit zterm t) end
-          | zterm (ZApp (t, u)) =
-              (ZApp (zterm t, Same.commit zterm u)
-                handle Same.SAME => ZApp (t, zterm u))
-          | zterm _ = raise Same.SAME;
-
         fun term (Var ((x, i), T)) =
               let val y = perhaps (Symtab.lookup vars) x
               in if x = y then raise Same.SAME else Var ((y, i), T) end
@@ -2276,8 +2263,7 @@
               in if x = y then Abs (x, T, term t) else Abs (y, T, Same.commit term t) end
           | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
           | term _ = raise Same.SAME;
-
-      in SOME {zterm = zterm, term = term} end
+      in SOME term end
   end;
 
 
@@ -2387,11 +2373,9 @@
       let val (As1, rder') =
         if lifted then
           (case rename_bvars dpairs tpairs B As0 of
-            SOME {zterm, term} =>
-              let
-                fun zproof p = ZTerm.map_proof Same.same zterm p;
-                fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p;
-              in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 zproof proof rder) end
+            SOME term =>
+              let fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p;
+              in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 I proof rder) end
           | NONE => (As0, rder))
         else (As0, rder);
       in