diff -r 09aee7f5b447 -r 308baf6b450a src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Dec 09 16:13:36 2019 +0000
+++ b/src/HOL/Library/Ramsey.thy	Mon Dec 09 16:37:26 2019 +0000
@@ -602,20 +602,20 @@
 qed
 
 
-subsubsection \<open>Partitions of a Set\<close>
+subsubsection \<open>Partition functions\<close>
 
-definition part :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
+definition part_fn :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
   \<comment> \<open>the function \<^term>\<open>f\<close> partitions the \<^term>\<open>r\<close>-subsets of the typically
       infinite set \<^term>\<open>Y\<close> into \<^term>\<open>s\<close> distinct categories.\<close>
-  where "part r s Y f \<longleftrightarrow> (\<forall>X \<in> nsets Y r. f X < s)"
+  where "part_fn r s Y f \<longleftrightarrow> (f \<in> nsets Y r \<rightarrow> {..<s})"
 
 text \<open>For induction, we decrease the value of \<^term>\<open>r\<close> in partitions.\<close>
-lemma part_Suc_imp_part:
-  "\<lbrakk>infinite Y; part (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part r s (Y - {y}) (\<lambda>u. f (insert y u))"
-  by (simp add: part_def nsets_def subset_Diff_insert)
+lemma part_fn_Suc_imp_part_fn:
+  "\<lbrakk>infinite Y; part_fn (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part_fn r s (Y - {y}) (\<lambda>u. f (insert y u))"
+  by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert)
 
-lemma part_subset: "part r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part r s Y f"
-  unfolding part_def nsets_def by blast
+lemma part_fn_subset: "part_fn r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part_fn r s Y f"
+  unfolding part_fn_def nsets_def by blast
 
 
 subsection \<open>Ramsey's Theorem: Infinitary Version\<close>
@@ -624,13 +624,13 @@
   fixes s r :: nat
     and YY :: "'a set"
     and f :: "'a set \<Rightarrow> nat"
-  assumes "infinite YY" "part r s YY f"
+  assumes "infinite YY" "part_fn r s YY f"
   shows "\<exists>Y' t'. Y' \<subseteq> YY \<and> infinite Y' \<and> t' < s \<and> (\<forall>X. X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> f X = t')"
   using assms
 proof (induct r arbitrary: YY f)
   case 0
   then show ?case
-    by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
+    by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong)
 next
   case (Suc r)
   show ?case
@@ -642,8 +642,8 @@
                  y \<in> YY \<and> y \<notin> Y \<and> Y \<subseteq> YY \<and> infinite Y \<and> t < s
                  \<and> (\<forall>X. X\<subseteq>Y \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert y) X = t)"
     from Suc.prems have infYY': "infinite (YY - {yy})" by auto
-    from Suc.prems have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
-      by (simp add: o_def part_Suc_imp_part yy)
+    from Suc.prems have partf': "part_fn r s (YY - {yy}) (f \<circ> insert yy)"
+      by (simp add: o_def part_fn_Suc_imp_part_fn yy)
     have transr: "trans ?ramr" by (force simp add: trans_def)
     from Suc.hyps [OF infYY' partf']
     obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
@@ -656,8 +656,8 @@
       with x obtain yx' where yx': "yx' \<in> Yx"
         by (blast dest: infinite_imp_nonempty)
       from fields x have infYx': "infinite (Yx - {yx'})" by auto
-      with fields x yx' Suc.prems have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
-        by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
+      with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f \<circ> insert yx')"
+        by (simp add: o_def part_fn_Suc_imp_part_fn part_fn_subset [where YY=YY and Y=Yx])
       from Suc.hyps [OF infYx' partfx'] obtain Y' and t'
         where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
           "X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'" for X
@@ -750,7 +750,7 @@
       \<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = r \<longrightarrow> f X < s\<rbrakk>
     \<Longrightarrow> \<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s
             \<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
-  by (blast intro: Ramsey_induction [unfolded part_def nsets_def])
+  by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def])
 
 
 corollary Ramsey2: