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.
more thorough beta contraction, following Envir.norm_term;
authorwenzelm
Tue, 19 Dec 2023 12:41:52 +0100
changeset 79300 236fa4b32afb
parent 79299 74a90157ee89
child 79301 4bb19eb09955
more thorough beta contraction, following Envir.norm_term;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle