--- a/src/HOL/WF.ML Fri Oct 17 15:23:14 1997 +0200
+++ b/src/HOL/WF.ML Fri Oct 17 15:25:12 1997 +0200
@@ -151,8 +151,7 @@
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)";
@@ -193,7 +192,7 @@
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 ***)