src/HOL/Power.thy

--- a/src/HOL/Power.thy	Thu Feb 12 17:43:53 1998 +0100
+++ b/src/HOL/Power.thy	Thu Feb 12 17:53:05 1998 +0100
@@ -19,7 +19,7 @@
   binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
 
   binomial_Suc "(Suc n choose k) =
-                (if k = 0 then 1 else (n choose pred k) + (n choose k))"
+                (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 end