changeset 52696 | 38466f4f3483 |
parent 52487 | 48bc24467008 |
child 52709 | 0e4bacf21e77 |
--- a/src/Pure/thm.ML Wed Jul 17 23:51:10 2013 +0200 +++ b/src/Pure/thm.ML Thu Jul 18 13:12:54 2013 +0200 @@ -569,7 +569,7 @@ fun future future_thm ct = let val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct; - val thy = Context.reject_draft (Theory.deref thy_ref); + val thy = Theory.deref thy_ref; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial ();