src/HOL/HOLCF/IOA/meta_theory/Traces.thy

                       then ~Enabled A W (laststate ex)
                       else is_wfair A W ex"
 
 is_wfair_def:
   "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
-                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
+                     | inf_often (%x. ~ Enabled A W (snd x)) (snd ex))"
 
 sfair_ex_def:
   "sfair_ex A ex == ! W : sfair_of A.
                       if   Finite (snd ex)
                       then ~Enabled A W (laststate ex)