diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Games.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -191,7 +191,7 @@
 
 definition "game = games_lfp"
 
-typedef (open) game = game
+typedef game = game
   unfolding game_def by (blast intro: games_lfp_nonempty)
 
 definition left_options :: "game \<Rightarrow> game zet" where
@@ -843,7 +843,7 @@
 
 definition "Pg = UNIV//eq_game_rel"
 
-typedef (open) Pg = Pg
+typedef Pg = Pg
   unfolding Pg_def by (auto simp add: quotient_def)
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"