src/HOL/WF.ML

 
 (*This rewrite rule works upon formulae; thus it requires explicit use of
   H_cong to expose the equality*)
 goalw WF.thy [cut_def]
     "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by (simp_tac (HOL_ss addsimps [expand_fun_eq]
-                    setloop (split_tac [expand_if])) 1);
+by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
 qed "cuts_eq";
 
 goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
 by (asm_simp_tac HOL_ss 1);
 qed "cut_apply";

 val gundef = recgb RS is_recfun_undef
 and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
 by (cut_facts_tac prems 1);
 by (rtac ext 1);
 by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
-                              setloop (split_tac [expand_if])) 1);
+                              addsplits [expand_if]) 1);
 qed "is_recfun_cut";
 
 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
 
 val prems = goalw WF.thy [the_recfun_def]