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
Thu, 07 Dec 2023 13:04:48 +0100
changeset 79173 de8c5cfe732e
parent 79172 0bea00f77ba3
child 79174 f91212703951
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle