changeset 79418 | 3a66bcb208b8 |
parent 79413 | 9495bd0112d7 |
child 79425 | 0875c87b4a4b |
--- a/src/Pure/thm.ML Tue Jan 02 23:17:43 2024 +0100 +++ b/src/Pure/thm.ML Wed Jan 03 12:40:10 2024 +0100 @@ -1100,7 +1100,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 map_ztyp zproof; + val zproof' = ZTerm.map_proof_types {hyps = false} 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',