--- a/src/HOL/Finite.ML Fri Oct 17 10:57:48 1997 +0200
+++ b/src/HOL/Finite.ML Fri Oct 17 10:58:44 1997 +0200
@@ -405,7 +405,6 @@
"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
by (etac finite_induct 1);
by (Simp_tac 1);
-by (Blast_tac 1);
by (Clarify_tac 1);
by (case_tac "x:A" 1);
(*1*)