src/Pure/Isar/skip_proof.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15667 b7bdc1651198
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -60,8 +60,8 @@
     1.4  fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
     1.5      (cheat_tac (ProofContext.theory_of ctxt))));
     1.6  
     1.7 -fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), None) x;
     1.8 -fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), None);
     1.9 +fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), NONE) x;
    1.10 +fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), NONE);
    1.11  
    1.12  end;
    1.13