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, following 8368160d3c65;
authorwenzelm
Mon, 18 Dec 2023 11:15:22 +0100
changeset 79276 18287f3f48ca
parent 79275 8368160d3c65
child 79277 7c415c73ebf7
proper treatment of proof hyps, following 8368160d3c65;
src/Pure/zterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/zterm.ML	Sun Dec 17 22:58:32 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 18 11:15:22 2023 +0100
@@ -314,7 +314,6 @@
 fun fold_proof_terms f =
   let
     fun proof (ZConstp (_, _, _, inst)) = ZVars.fold (f o #2) inst
-      | proof (ZHyp t) = f t
       | proof (ZAbst (_, _, p)) = proof p
       | proof (ZAbsp (_, t, p)) = f t #> proof p
       | proof (ZAppt (p, t)) = proof p #> f t
isabelle