src/HOL/ex/InSort.ML

 *)
 
 goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
 by (list.induct_tac "xs" 1);
 by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
 qed "mset_ins";
 Addsimps [mset_ins];
 
 goal thy "!x. mset(insort f xs) x = mset xs x";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "insort_permutes";
 
 goal thy "set(ins f x xs) = insert x (set xs)";
 by (asm_simp_tac (!simpset addsimps [set_via_mset]
-                           setloop (split_tac [expand_if])) 1);
+                           addsplits [expand_if]) 1);
 by (Fast_tac 1);
 qed "set_ins";
 Addsimps [set_ins];
 
 val prems = goalw InSort.thy [total_def,transf_def]
   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted_ins";
 Addsimps [sorted_ins];