src/Pure/Isar/skip_proof.ML

--- a/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -35,7 +35,7 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove thy xs asms prop tac =
-  Tactic.prove thy xs asms prop
+  Goal.prove thy xs asms prop
     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
 
 end;