# HG changeset patch
# User haftmann
# Date 1291133951 -3600
# Node ID f5a0cb45d2a559959927df7e6003329bd92147b5
# Parent  37b25a87d7ef032fcb9498c007b644136c0f53e9
adapted fragile proof

diff -r 37b25a87d7ef -r f5a0cb45d2a5 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Tue Nov 30 17:19:11 2010 +0100
+++ b/src/HOL/ZF/Games.thy	Tue Nov 30 17:19:11 2010 +0100
@@ -893,9 +893,9 @@
   have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" 
     apply (simp add: congruent2_def)
     apply (auto simp add: eq_game_rel_def eq_game_def)
-    apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
+    apply (rule_tac y="plus_game a ba" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
-    apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
+    apply (rule_tac y="plus_game b aa" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
     done
   then show ?thesis