# HG changeset patch
# User wenzelm
# Date 1702850312 -3600
# Node ID 8368160d3c6539108f8619bac8156e2e21576ed7
# Parent  fb8ed7fbb537313bad3b9a99ff5df5bef2f36ac2
proper treatment of proof hyps: unchangeable, like bound;

diff -r fb8ed7fbb537 -r 8368160d3c65 src/Pure/zterm.ML
--- 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)) =