src/Pure/Isar/skip_proof.ML
changeset 17956 369e2af8ee45
parent 17476 315cb57e3dd7
child 18708 4b3dadb4fe33
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:32 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Oct 21 18:14:34 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     1.5  
     1.6  fun prove thy xs asms prop tac =
     1.7 -  Tactic.prove thy xs asms prop
     1.8 +  Goal.prove thy xs asms prop
     1.9      (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
    1.10  
    1.11  end;