--- a/src/HOL/Finite.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Finite.ML Tue Dec 16 17:58:03 1997 +0100
@@ -65,7 +65,7 @@
val lemma = result();
goal Finite.thy "!!A. [| A<=B; finite B |] ==> finite A";
-bd lemma 1;
+by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_subset";