prove: setmp quick_and_dirty (avoids race condition);
authorwenzelm
Fri Aug 31 18:46:37 2007 +0200 (2007-08-31 ago)
changeset 245028d5326f0098b
parent 24501 7a2b20145888
child 24503 2439587f516b
prove: setmp quick_and_dirty (avoids race condition);
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Aug 31 18:46:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Aug 31 18:46:37 2007 +0200
     1.3 @@ -36,7 +36,9 @@
     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 -  Goal.prove ctxt xs asms prop
     1.8 -    (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
     1.9 +  Goal.prove ctxt xs asms prop (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
    1.12 +    else tac args st);
    1.13  
    1.14  end;