src/HOL/MiniML/W.ML

 by (eresolve_tac has_type_casesE 1);
 by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
-by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong] 
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong] 
     setloop (split_tac [expand_option_bind]))) 1);
 
 (* case App e1 e2 *)
 by (strip_tac 1);
 by (eresolve_tac has_type_casesE 1);