src/HOL/HOLCF/FOCUS/Buffer_adm.thy

--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 27 22:20:07 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 27 23:06:59 2011 +0100
@@ -254,7 +254,7 @@
 apply (clarsimp)
 apply (drule (1) fstream_lub_lemma)
 apply (clarsimp)
-apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1")
+apply (simp only: ex_simps [symmetric] all_simps [symmetric])
 apply (rule_tac x="Xa" in exI)
 apply (rule allI)
 apply (rotate_tac -1)