src/Pure/Isar/skip_proof.ML
changeset 28446 a01de3b3fa2e
parent 28365 6249297461cb
child 28552 f8719bcc5006
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:00:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:18:18 2008 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     1.5  
     1.6  fun prove ctxt xs asms prop tac =
     1.7 -  (if ! future_scheduler then Goal.prove_promise else Goal.prove) ctxt xs asms prop
     1.8 +  (if ! future_scheduler then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.9      (fn args => fn st =>
    1.10        if ! quick_and_dirty
    1.11        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st