1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:39:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:47:51 2012 +0200
     1.3 @@ -704,10 +704,11 @@
     1.4  
     1.5  val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
     1.6  
     1.7 -val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
     1.8 +val parse_binding_colon = Parse.binding --| @{keyword ":"};
     1.9 +val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
    1.10  
    1.11  val parse_ctr_arg =
    1.12 -  @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
    1.13 +  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
    1.14    (Parse.typ >> pair no_binder);
    1.15  
    1.16  val parse_defaults =