# HG changeset patch
# User wenzelm
# Date 1701950688 -3600
# Node ID de8c5cfe732e4f2cb2435bcfe461ef42121eacad
# Parent  0bea00f77ba36bacfbf07ad6335c07a49b7a16e0
tuned;

diff -r 0bea00f77ba3 -r de8c5cfe732e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 07 12:12:13 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 13:04:48 2023 +0100
@@ -752,7 +752,7 @@
           (AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf)
             handle Same.SAME => AbsP (s, t, norm prf))
       | norm (prf % t) =
-          (norm prf % Option.map (htype Envir.norm_term) t
+          (norm prf % Option.map (Same.commit (htype Envir.norm_term_same)) t
             handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t)
       | norm (prf1 %% prf2) =
           (norm prf1 %% Same.commit norm prf2