src/HOL/Divides.ML

--- a/src/HOL/Divides.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Divides.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -222,7 +222,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 setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "mod2_cases";