# HG changeset patch
# User wenzelm
# Date 1702986243 -3600
# Node ID 4bb19eb099550cafa604dfd6e351890cf67d21f9
# Parent  236fa4b32afb14dcf7e85fea5323d05a7ab3f6cc
tuned;

diff -r 236fa4b32afb -r 4bb19eb09955 src/Pure/zterm.ML
--- 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)