choose just as an infix

--- 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"