--- a/src/HOL/Library/Ramsey.thy Thu Nov 13 15:58:37 2008 +0100
+++ b/src/HOL/Library/Ramsey.thy Thu Nov 13 15:58:38 2008 +0100
@@ -131,8 +131,8 @@
from dependent_choice [OF transr propr0 proprstep]
obtain g where pg: "!!n::nat. ?propr (g n)"
and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
- let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"
- let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"
+ let ?gy = "fst o g"
+ let ?gt = "snd o snd o g"
have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
proof (intro exI subsetI)
fix x