diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri May 13 22:55:00 2011 +0200
@@ -83,9 +83,9 @@
 lemma last_ind_on_first:
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
-  apply (tactic {* auto_tac (@{claset},
+  apply (tactic {* auto_tac (map_simpset_local (fn _ =>
     HOL_ss addsplits [@{thm list.split}]
-    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
+    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
   done
 
 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}