Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 19 Dec 2023 12:44:03 +0100
changeset 79301 4bb19eb09955
parent 79300 236fa4b32afb
child 79302 fed9791928bf
tuned;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/zterm.ML	Tue Dec 19 12:41:52 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 12:44:03 2023 +0100
@@ -600,12 +600,12 @@
           (ZAbsp (a, term t, Same.commit norm p)
             handle Same.SAME => ZAbsp (a, t, norm p))
       | norm (ZAppt (ZAbst (_, _, body), t)) = Same.commit norm (subst_proof_bound t body)
+      | norm (ZAppp (ZAbsp (_, _, body), p)) = Same.commit norm (subst_proof_boundp p body)
       | norm (ZAppt (f, t)) =
           ((case norm f of
              ZAbst (_, _, body) => Same.commit norm (subst_proof_bound t body)
            | nf => ZAppt (nf, Same.commit term t))
           handle Same.SAME => ZAppt (f, term t))
-      | norm (ZAppp (ZAbsp (_, _, body), p)) = Same.commit norm (subst_proof_boundp p body)
       | norm (ZAppp (f, p)) =
           ((case norm f of
              ZAbsp (_, _, body) => Same.commit norm (subst_proof_boundp p body)
isabelle