desambiguate grammar (e.g. for Nil's mixfix ("[]"))

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:39:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:47:51 2012 +0200
@@ -704,10 +704,11 @@
 
 val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
 
-val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
 
 val parse_ctr_arg =
-  @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
+  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   (Parse.typ >> pair no_binder);
 
 val parse_defaults =