src/HOL/Induct/Mutil.ML
changeset 3414 804c8a178a7f
parent 3357 c224dddc5f71
child 3423 3684a4420a67
--- a/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:39:22 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML	Thu Jun 05 14:40:35 1997 +0200
@@ -117,8 +117,7 @@
 qed "domino_singleton";
 
 goal thy "!!d. d:domino ==> finite d";
-by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
-                      addSEs [domino.elim]) 1);
+by (blast_tac (!claset addSEs [domino.elim]) 1);
 qed "domino_finite";
 
 
@@ -126,7 +125,7 @@
 
 goal thy "!!t. t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
-by (rtac finite_emptyI 1);
+by (rtac Finites.emptyI 1);
 by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
 qed "tiling_domino_finite";