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 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',
isabelle