# HG changeset patch
# User wenzelm
# Date 1704974979 -3600
# Node ID 64b3cfbce63fee9f6b8107365deb1269bcabed4d
# Parent  9eb9882f184569dd4ef64883e78755ab7508e47b
tuned;

diff -r 9eb9882f1845 -r 64b3cfbce63f src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jan 11 12:44:27 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 11 13:09:39 2024 +0100
@@ -200,11 +200,11 @@
     ZDummy                         (*dummy proof*)
   | ZConstp of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
   | ZBoundp of int
-  | ZHyp of zterm
   | ZAbst of string * ztyp * zproof
   | ZAbsp of string * zterm * zproof
   | ZAppt of zproof * zterm
   | ZAppp of zproof * zproof
+  | ZHyp of zterm
   | ZClassp of ztyp * class;       (*OFCLASS proof from sorts algebra*)
 
 
@@ -478,11 +478,11 @@
       | proof (ZConstp (_, _, instT, inst)) =
           ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst
       | proof (ZBoundp _) = I
-      | proof (ZHyp h) = hyps ? term h
       | proof (ZAbst (_, T, p)) = typ T #> proof p
       | proof (ZAbsp (_, t, p)) = term t #> proof p
       | proof (ZAppt (p, t)) = proof p #> term t
       | proof (ZAppp (p, q)) = proof p #> proof q
+      | proof (ZHyp h) = hyps ? term h
       | proof (ZClassp (T, _)) = hyps ? typ T;
   in proof end;
 
@@ -537,7 +537,6 @@
           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) = if hyps then ZHyp (term h) else raise Same.SAME
       | proof (ZAbst (a, T, p)) =
           (ZAbst (a, typ T, Same.commit proof p)
             handle Same.SAME => ZAbst (a, T, proof p))
@@ -550,6 +549,7 @@
       | proof (ZAppp (p, q)) =
           (ZAppp (proof p, Same.commit proof q)
             handle Same.SAME => ZAppp (p, proof q))
+      | proof (ZHyp h) = if hyps then ZHyp (term h) else raise Same.SAME
       | proof (ZClassp (T, c)) = if hyps then ZClassp (typ T, c) else raise Same.SAME;
   in proof end;