src/HOL/Wellfounded_Relations.ML

--- a/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/Wellfounded_Relations.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -143,7 +143,7 @@
  by (etac exE 1);
  by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
  by (Blast_tac 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);