diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -41,13 +41,13 @@
 (* basic cheating *)
 
 fun make_thm thy t =
-  Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
+  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
 
 fun cheat_tac thy st =
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove thy xs asms prop tac =
-  Tactic.prove (Theory.sign_of thy) xs asms prop
+  Tactic.prove thy xs asms prop
     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);