Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 79273 d1e5f6d1ddca
parent 79270 90c5aadcc4b2
child 79279 d9a7ee1bd070 
--- a/src/Pure/thm.ML	Sun Dec 17 21:34:44 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 17 21:43:14 2023 +0100
@@ -2395,7 +2395,7 @@
           (case rename_bvars dpairs tpairs B As0 of
             SOME {zterm, term} =>
               let
-                fun zproof p = Same.commit (ZTerm.map_proof_same Same.same zterm) p;
+                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
           | NONE => (As0, rder))
isabelle