diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/NTP/Correctness.ML
--- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
 (* Proof of correctness *)
 goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
   "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by (simp_tac (simpset() delsplits [expand_if] addsimps 
+by (simp_tac (simpset() delsplits [split_if] addsimps 
     [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
 by (rtac conjI 1);
  by (simp_tac ss' 1);
@@ -77,7 +77,7 @@
 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
 
 by (Action.action.induct_tac "a"  1);
-by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (ss' addsplits [split_if]) 1);
 by (forward_tac [inv4] 1);
 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
 by (simp_tac ss' 1);