1.1 --- a/src/HOL/ZF/Games.thy	Mon Aug 01 20:21:11 2011 +0200
     1.2 +++ b/src/HOL/ZF/Games.thy	Tue Aug 02 10:03:12 2011 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4    apply (simp add: wfzf_is_option_of)
     1.5    done
     1.6  
     1.7 -lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
     1.8 +lemma wf_option_of[simp, intro]: "wf option_of"
     1.9  proof -
    1.10    have option_of: "option_of = inv_image is_option_of Rep_game"
    1.11      apply (rule set_eqI)