equal
deleted
inserted
replaced
828 |
828 |
829 fun box_proof {unconstrain} zproof_name thy hyps concl prf = |
829 fun box_proof {unconstrain} zproof_name thy hyps concl prf = |
830 let |
830 let |
831 val {zterm, ...} = zterm_cache thy; |
831 val {zterm, ...} = zterm_cache thy; |
832 |
832 |
833 val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl); |
833 val present_set = Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps); |
834 val ucontext as {constraints, outer_constraints, ...} = |
834 val ucontext as {constraints, outer_constraints, ...} = |
835 Logic.unconstrain_context [] present_set; |
835 Logic.unconstrain_context [] present_set; |
836 |
836 |
837 val typ_operation = #typ_operation ucontext {strip_sorts = true}; |
837 val typ_operation = #typ_operation ucontext {strip_sorts = true}; |
838 val unconstrain_typ = Same.commit typ_operation; |
838 val unconstrain_typ = Same.commit typ_operation; |