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.
proper treatment of ZConstP: term represents body of closure;
authorwenzelm
Wed, 06 Dec 2023 15:21:00 +0100
changeset 79148 99201e7b1d94
parent 79147 bfe5c20074e4
child 79149 810679c5ed3c
proper treatment of ZConstP: term represents body of closure;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/zterm.ML	Wed Dec 06 15:15:14 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 15:21:00 2023 +0100
@@ -269,9 +269,8 @@
   let
     fun proof ZDummy = raise Same.SAME
       | proof (ZConstP (a, A, instT, inst)) =
-          (case Same.catch (map_insts_same typ term) (instT, inst) of
-            NONE => ZConstP (a, term A, instT, inst)
-          | SOME (instT', inst') => ZConstP (a, Same.commit term A, instT', inst'))
+          let val (instT', inst') = map_insts_same typ term (instT, inst)
+          in ZConstP (a, A, instT', inst') end
       | proof (ZBoundP _) = raise Same.SAME
       | proof (ZHyp h) = ZHyp (term h)
       | proof (ZAbst (a, T, p)) =
isabelle