src/HOL/Induct/Mutil.ML

--- a/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:15:39 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:16:04 1998 +0200
@@ -152,7 +152,7 @@
 (*Cardinality is smaller because of the two elements fewer*)
 by (rtac less_trans 1);
 by (REPEAT
-    (rtac card_Diff 1 
+    (rtac card_Diff1_less 1 
      THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
      THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1));
 qed "mutil_not_tiling";