diff -r 94e0fdcb7b91 -r c036caebfc75 src/HOL/MiniML/Instance.ML --- a/src/HOL/MiniML/Instance.ML Fri Oct 17 15:23:14 1997 +0200 +++ b/src/HOL/MiniML/Instance.ML Fri Oct 17 15:25:12 1997 +0200 @@ -66,8 +66,8 @@ by (rename_tac "S1 S2" 1); by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1); by (safe_tac (!claset)); -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 (strip_tac 1); by (dres_inst_tac [("x","x")] bspec 1); by (assume_tac 1); @@ -82,8 +82,8 @@ goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \ \ (bound_typ_inst (%k. TVar (k + n)) sch) = sch"; by (type_scheme.induct_tac "sch" 1); -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1); -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 1); +by (simp_tac (!simpset addsimps [leD] addsplits [expand_if]) 1); +by (simp_tac (!simpset addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1); by (Asm_simp_tac 1); qed_spec_mp "subst_to_scheme_inverse"; @@ -96,9 +96,9 @@ \ (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)"; by (type_scheme.induct_tac "sch" 1); -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1); +by (simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1); by (Asm_simp_tac 1); -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1); +by (asm_full_simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1); val aux2 = result () RS mp;