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/Proof/extraction.ML
changeset 79167 4fb0723dc5fc
parent 79114 686b7b14d041
child 79175 04dfecb9343a 
--- a/src/Pure/Proof/extraction.ML	Thu Dec 07 10:40:59 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Dec 07 10:46:49 2023 +0100
@@ -567,7 +567,7 @@
           in (
             if T = nullT then AbsP ("R",
               SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
-                Proofterm.prf_subst_bounds [nullt] corr_prf)
+                Proofterm.subst_bounds [nullt] corr_prf)
             else Abst (s, SOME T, AbsP ("R",
               SOME (app_rlz_rews (T :: Ts) vs
                 (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)), defs')
isabelle