diff -r 3daeda3d3cd0 -r 1d097572d23b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Mon Oct 09 12:23:45 2000 +0200
+++ b/src/HOL/Nat.ML	Mon Oct 09 12:24:12 2000 +0200
@@ -58,7 +58,7 @@
 
 Goal "!!n::nat. (~(0 < n)) = (n=0)";
 by (rtac iffI 1);
- by (etac swap 1);
+ by (rtac ccontr 1);
  by (ALLGOALS Asm_full_simp_tac);
 qed "not_gr0";
 AddIffs [not_gr0];