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 proof hyps: unchangeable, like bound;
authorwenzelm
Sun, 17 Dec 2023 22:58:32 +0100
changeset 79275 8368160d3c65
parent 79274 fb8ed7fbb537
child 79276 18287f3f48ca
proper treatment of proof hyps: unchangeable, like bound;
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)) =
isabelle