diff -r 9733ab5c1df6 -r 7b9336176a1c src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Nov 25 10:20:25 2013 +0100
+++ b/src/HOL/Library/Ramsey.thy	Mon Nov 25 12:27:03 2013 +0100
@@ -247,7 +247,7 @@
     then obtain s' and n'
       where s': "s' = ?gt n'"
         and infeqs': "infinite {n. ?gt n = s'}"
-      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
+      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
     have inj_gy: "inj ?gy"
     proof (rule linorder_injI)
@@ -410,7 +410,7 @@
   have
    "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
           (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
-    by (rule Ramsey2) (auto intro: trless nat_infinite)
+    by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
   then obtain K and k
     where infK: "infinite K" and less: "k < n" and
           allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"