diff -r 17d1e32ef867 -r a1960091c34d src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Sun Feb 15 22:58:02 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Feb 16 13:38:08 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Binomial.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Amine Chaieb
     Copyright   1997  University of Cambridge
 *)
@@ -13,11 +12,9 @@
 text {* This development is based on the work of Andy Gordon and
   Florian Kammueller. *}
 
-consts
-  binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
-primrec
+primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where
   binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
-  binomial_Suc: "(Suc n choose k) =
+  | binomial_Suc: "(Suc n choose k) =
                  (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"