| changeset 52696 | 38466f4f3483 |
| parent 52607 | 33a133d50616 |
| child 52710 | 52790e3961fe |
--- a/src/Pure/goal.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/goal.ML Thu Jul 18 13:12:54 2013 +0200 @@ -232,7 +232,6 @@ fun future_result ctxt result prop = let val thy = Proof_Context.theory_of ctxt; - val _ = Context.reject_draft thy; val cert = Thm.cterm_of thy; val certT = Thm.ctyp_of thy;