src/HOL/Library/Ramsey.thy

     have "finite (range ?gt)"
       by (simp add: finite_nat_iff_bounded rangeg)
     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)
       fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
         using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto

     apply (blast dest: s_in_T transition_idx_less)
     done
   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"
     by auto
   have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"