# HG changeset patch
# User wenzelm
# Date 1704973030 -3600
# Node ID c39aed404ffc80b330b4075122786c88d904c7c9
# Parent  e1b2595d678a80bd3daa640143708679e2657cb0
more uniform treatment of "hyps" within zproof;

diff -r e1b2595d678a -r c39aed404ffc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jan 11 12:00:02 2024 +0100
+++ b/src/Pure/thm.ML	Thu Jan 11 12:37:10 2024 +0100
@@ -1103,7 +1103,7 @@
           ZTypes.unsynchronized_cache
             (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
 
-        val zproof' = ZTerm.map_proof_types {hyps = false} map_ztyp zproof;
+        val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
         val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
       in
         Thm (make_deriv promises oracles thms zboxes zproof' proof',
diff -r e1b2595d678a -r c39aed404ffc src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jan 11 12:00:02 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 11 12:37:10 2024 +0100
@@ -530,7 +530,7 @@
       | proof (ZAppp (p, q)) =
           (ZAppp (proof p, Same.commit proof q)
             handle Same.SAME => ZAppp (p, proof q))
-      | proof (ZClassp (T, c)) = ZClassp (typ T, c);
+      | proof (ZClassp (T, c)) = if hyps then ZClassp (typ T, c) else raise Same.SAME;
   in proof end;
 
 fun map_proof hyps typ term = Same.commit (map_proof_same hyps typ term);