src/Pure/thm.ML
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 ();