1.1 --- a/src/HOL/Library/Ramsey.thy	Mon Nov 25 10:20:25 2013 +0100
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Mon Nov 25 12:27:03 2013 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4      then obtain s' and n'
     1.5        where s': "s' = ?gt n'"
     1.6          and infeqs': "infinite {n. ?gt n = s'}"
     1.7 -      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
     1.8 +      by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
     1.9      with pg [of n'] have less': "s'<s" by (cases "g n'") auto
    1.10      have inj_gy: "inj ?gy"
    1.11      proof (rule linorder_injI)
    1.12 @@ -410,7 +410,7 @@
    1.13    have
    1.14     "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
    1.15            (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
    1.16 -    by (rule Ramsey2) (auto intro: trless nat_infinite)
    1.17 +    by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
    1.18    then obtain K and k
    1.19      where infK: "infinite K" and less: "k < n" and
    1.20            allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"

     2.1 --- a/src/HOL/NSA/StarDef.thy	Mon Nov 25 10:20:25 2013 +0100
     2.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Nov 25 12:27:03 2013 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  apply (unfold FreeUltrafilterNat_def)
     2.5  apply (rule someI_ex)
     2.6  apply (rule freeultrafilter_Ex)
     2.7 -apply (rule nat_infinite)
     2.8 +apply (rule infinite_UNIV_nat)
     2.9  done
    2.10  
    2.11  interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat