# HG changeset patch
# User wenzelm
# Date 1702986112 -3600
# Node ID 236fa4b32afb14dcf7e85fea5323d05a7ab3f6cc
# Parent  74a90157ee89e5a5c05fa1a9d755080d50fefa16
more thorough beta contraction, following Envir.norm_term;

diff -r 74a90157ee89 -r 236fa4b32afb src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 12:35:24 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 12:41:52 2023 +0100
@@ -595,7 +595,11 @@
   let
     val term = beta_norm_term_same;
 
-    fun norm (ZAppt (ZAbst (_, _, body), t)) = Same.commit norm (subst_proof_bound t body)
+    fun norm (ZAbst (a, T, p)) = ZAbst (a, T, norm p)
+      | norm (ZAbsp (a, t, p)) =
+          (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 (ZAppt (f, t)) =
           ((case norm f of
              ZAbst (_, _, body) => Same.commit norm (subst_proof_bound t body)