src/HOL/Library/Ramsey.thy
changeset 28741 1b257449f804
parent 27487 c8a6ce181805
child 30738 0842e906300c
     1.1 --- a/src/HOL/Library/Ramsey.thy	Thu Nov 13 15:58:37 2008 +0100
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Thu Nov 13 15:58:38 2008 +0100
     1.3 @@ -131,8 +131,8 @@
     1.4      from dependent_choice [OF transr propr0 proprstep]
     1.5      obtain g where pg: "!!n::nat.  ?propr (g n)"
     1.6        and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
     1.7 -    let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"
     1.8 -    let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"
     1.9 +    let ?gy = "fst o g"
    1.10 +    let ?gt = "snd o snd o g"
    1.11      have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    1.12      proof (intro exI subsetI)
    1.13        fix x