# HG changeset patch
# User wenzelm
# Date 1702894522 -3600
# Node ID 18287f3f48ca10e277b7c02cf390f109eb116015
# Parent  8368160d3c6539108f8619bac8156e2e21576ed7
proper treatment of proof hyps, following 8368160d3c65;

diff -r 8368160d3c65 -r 18287f3f48ca src/Pure/zterm.ML
--- 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