--- a/src/HOLCF/IOA/Modelcheck/Ring3.ML	Fri Aug 20 16:16:02 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.ML	Fri Aug 20 16:16:16 1999 +0200
@@ -8,9 +8,6 @@
 (* property to prove: at most one (of 3) members of the ring will
 	declare itself to leader *)
 Goal "ring =<| one_leader";
-(*
-FIXME
 by (is_sim_tac aut_simps 1); 
 by Auto_tac;
 qed"at_most_one_leader";
-*)