equal
deleted
inserted
replaced
2240 map OfClass (#outer_constraints ucontext) @ map Hyp hyps); |
2240 map OfClass (#outer_constraints ucontext) @ map Hyp hyps); |
2241 in (thm, proof) end; |
2241 in (thm, proof) end; |
2242 |
2242 |
2243 in |
2243 in |
2244 |
2244 |
2245 val thm_proof = prepare_thm_proof false; |
2245 fun thm_proof thy = prepare_thm_proof false thy; |
2246 |
2246 |
2247 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body = |
2247 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body = |
2248 prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none) |
2248 prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none) |
2249 shyps [] concl promises body; |
2249 shyps [] concl promises body; |
2250 |
2250 |