author | wenzelm |
Sun, 17 Dec 2023 22:58:32 +0100 | |
changeset 79275 | 8368160d3c65 |
parent 79274 | fb8ed7fbb537 |
child 79276 | 18287f3f48ca |
src/Pure/zterm.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/zterm.ML Sun Dec 17 22:57:20 2023 +0100 +++ b/src/Pure/zterm.ML Sun Dec 17 22:58:32 2023 +0100 @@ -444,7 +444,7 @@ 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 (ZHyp _) = raise Same.SAME | proof (ZAbst (a, T, p)) = (ZAbst (a, typ T, Same.commit proof p) handle Same.SAME => ZAbst (a, T, proof p)) | proof (ZAbsp (a, t, p)) =