diff -r 76c5f277b234 -r f2a587696afb src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Nov 23 22:59:39 2011 +0100
@@ -84,8 +84,9 @@
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
   apply (tactic {* auto_tac (map_simpset (fn _ =>
-    HOL_ss addsplits [@{thm list.split}]
-    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
+    HOL_ss
+    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])
+    |> Splitter.add_split @{thm list.split}) @{context}) *})
   done
 
 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}