src/HOL/ZF/Games.thy

--- a/src/HOL/ZF/Games.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/ZF/Games.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -323,7 +323,7 @@
 lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
 proof -
   have option_of: "option_of = inv_image is_option_of Rep_game"
-    apply (rule set_ext)
+    apply (rule set_eqI)
     apply (case_tac "x")
     by (simp add: option_to_is_option_of) 
   show ?thesis