author | wenzelm |
Wed, 16 Oct 2019 15:31:01 +0200 | |
changeset 70887 | de6f137a07d3 |
parent 70886 | ca7831201a7a |
child 70888 | 9ff9559f1ee2 |
--- a/src/Pure/proofterm.ML Wed Oct 16 12:42:09 2019 +0200 +++ b/src/Pure/proofterm.ML Wed Oct 16 15:31:01 2019 +0200 @@ -2242,7 +2242,7 @@ in -val thm_proof = prepare_thm_proof false; +fun thm_proof thy = prepare_thm_proof false thy; fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body = prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)