src/HOL/MiniML/Generalize.ML

--- a/src/HOL/MiniML/Generalize.ML	Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Fri Oct 17 15:25:12 1997 +0200
@@ -45,8 +45,8 @@
 by (typ.induct_tac "t1" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
 by (Fast_tac 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
@@ -99,7 +99,7 @@
 by (rename_tac "R" 1);
 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
 by (typ.induct_tac "t" 1);
- by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+ by (simp_tac (!simpset addsplits [expand_if]) 1);
 by (Asm_simp_tac 1);
 qed "gen_bound_typ_instance";
 
@@ -109,7 +109,7 @@
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
 by (typ.induct_tac "t" 1);
- by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+ by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
  by (Fast_tac 1);
 by (Asm_simp_tac 1);
 qed "free_tv_subset_gen_le";
@@ -123,8 +123,8 @@
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
 by (subgoal_tac "n <= n + nat" 1);
 by (forw_inst_tac [("t","A")] new_tv_le 1);
 by (assume_tac 1);