diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/ZF/Games.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -831,10 +831,10 @@
   Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
 
 definition
-  Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+  Pg_minus_def: "- G = the_elem (\<Union>g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
 
 definition
-  Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
+  Pg_plus_def: "G + H = the_elem (\<Union>g \<in> Rep_Pg G. \<Union>h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
 
 definition
   Pg_diff_def: "G - H = G + (- (H::Pg))"