--- 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. *}