diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/Induct/Com.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -53,7 +53,7 @@
 
 goalw thy [assign_def] "s[s x/x] = s";
 by (rtac ext 1);
-by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
+by (simp_tac (!simpset addsplits [expand_if]) 1);
 qed "assign_triv";
 
 Addsimps [assign_same, assign_different, assign_triv];