src/HOL/Library/Ramsey.thy

             using fields Y' yx' px by blast
         qed
       qed
     qed
     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
+    obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
+      by blast
     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