--- a/src/HOL/Power.thy Wed Oct 13 12:07:03 1999 +0200
+++ b/src/HOL/Power.thy Wed Oct 13 12:07:23 1999 +0200
@@ -9,7 +9,7 @@
Power = Divides +
consts
- binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50])
+ binomial :: "[nat,nat] => nat" (infixl "choose" 65)
primrec
"p ^ 0 = 1"