1.1 --- a/src/HOL/Induct/Mutil.ML	Wed Mar 22 13:01:18 2000 +0100
     1.2 +++ b/src/HOL/Induct/Mutil.ML	Wed Mar 22 13:01:57 2000 +0100
     1.3 @@ -104,9 +104,9 @@
     1.4  by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
     1.5  qed "domino_singleton";
     1.6  
     1.7 -Goal "d:domino \
     1.8 -\     ==> EX i j i' j'. colored 0 d = {(i,j)} & colored 1 d = {(i',j')}";
     1.9 -by (blast_tac (claset() addDs [domino_singleton]) 1);
    1.10 +Goal "d:domino ==> (EX i j. colored 0 d = {(i,j)}) & \
    1.11 +\                  (EX i' j'. colored 1 d = {(i',j')})";
    1.12 +by (blast_tac (claset() addSIs [domino_singleton]) 1);
    1.13  qed "domino_singleton_01";
    1.14  
    1.15  (*** Tilings of dominoes ***)