# HG changeset patch
# User traytel
# Date 1385378823 -3600
# Node ID 7b9336176a1cba27fd784a87208a9ecb86688426
# Parent  9733ab5c1df6544523dce03d28544c0f09cb964a
adapt to 9733ab5c1df6

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"
diff -r 9733ab5c1df6 -r 7b9336176a1c src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Nov 25 10:20:25 2013 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Nov 25 12:27:03 2013 +0100
@@ -18,7 +18,7 @@
 apply (unfold FreeUltrafilterNat_def)
 apply (rule someI_ex)
 apply (rule freeultrafilter_Ex)
-apply (rule nat_infinite)
+apply (rule infinite_UNIV_nat)
 done
 
 interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat