diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/IOA/Modelcheck/Ring3.thy
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy	Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Fri Mar 20 17:12:37 2009 +0100
@@ -114,7 +114,7 @@
 (* property to prove: at most one (of 3) members of the ring will
 	declare itself to leader *)
 lemma at_most_one_leader: "ring =<| one_leader"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
 apply auto
 done