# HG changeset patch
# User wenzelm
# Date 1701872460 -3600
# Node ID 99201e7b1d9416c861f2b03e758ff31d8db6a445
# Parent  bfe5c20074e48aee7fc9588a0a6919a35c62b97a
proper treatment of ZConstP: term represents body of closure;

diff -r bfe5c20074e4 -r 99201e7b1d94 src/Pure/zterm.ML
--- 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)) =