src/ZF/ex/Mutil.ML

--- a/src/ZF/ex/Mutil.ML	Tue Mar 10 19:02:20 1998 +0100
+++ b/src/ZF/ex/Mutil.ML	Tue Mar 10 19:02:53 1998 +0100
@@ -131,7 +131,7 @@
                                   dominoes_tile_matrix]) 2);
 by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1);
 by (asm_simp_tac (simpset() addsimps add_ac) 2);
-by (asm_full_simp_tac 
+by (asm_lr_simp_tac 
     (simpset() addsimps [evnodd_Diff, mod2_add_self,
                         mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
 by (rtac lt_trans 1);