# HG changeset patch
# User paulson
# Date 953726517 -3600
# Node ID a79f6fb4d426165f927d6ea812444a1bc4eca0ec
# Parent  8c4ff19a7286a611a12330ca5b078b8ff7be3ddf
made more robust

diff -r 8c4ff19a7286 -r a79f6fb4d426 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Wed Mar 22 13:01:18 2000 +0100
+++ b/src/HOL/Induct/Mutil.ML	Wed Mar 22 13:01:57 2000 +0100
@@ -104,9 +104,9 @@
 by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
 qed "domino_singleton";
 
-Goal "d:domino \
-\     ==> EX i j i' j'. colored 0 d = {(i,j)} & colored 1 d = {(i',j')}";
-by (blast_tac (claset() addDs [domino_singleton]) 1);
+Goal "d:domino ==> (EX i j. colored 0 d = {(i,j)}) & \
+\                  (EX i' j'. colored 1 d = {(i',j')})";
+by (blast_tac (claset() addSIs [domino_singleton]) 1);
 qed "domino_singleton_01";
 
 (*** Tilings of dominoes ***)