Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 79474 c39aed404ffc
parent 79454 6b6e9af552f5 
--- 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',
isabelle