src/HOL/Divides.ML

--- a/src/HOL/Divides.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Divides.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -229,7 +229,7 @@
 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by Safe_tac;
 qed "mod2_cases";