diff -r 19356bb4a0db -r c422ef7b9fae src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Mon Feb 23 14:48:17 2015 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Mon Feb 23 14:48:40 2015 +0100
@@ -614,7 +614,7 @@
 text{*Versions of the theorems above for the natural-number version of "choose"*}
 lemma binomial_altdef_of_nat:
   fixes n k :: nat
-    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}}*}
+    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
   assumes "k \<le> n"
   shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
 using assms