1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -41,13 +41,13 @@
     1.4  (* basic cheating *)
     1.5  
     1.6  fun make_thm thy t =
     1.7 -  Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
     1.8 +  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
     1.9  
    1.10  fun cheat_tac thy st =
    1.11    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    1.12  
    1.13  fun prove thy xs asms prop tac =
    1.14 -  Tactic.prove (Theory.sign_of thy) xs asms prop
    1.15 +  Tactic.prove thy xs asms prop
    1.16      (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    1.17  
    1.18