Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/zterm.ML
changeset 79148 99201e7b1d94
parent 79147 bfe5c20074e4
child 79149 810679c5ed3c 
--- 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