src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51787 1267c28c7bdd
parent 51781 0504e286d66d
child 51788 5fe72280a49f
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 09:53:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:45 2013 +0200
     1.3 @@ -1224,7 +1224,8 @@
     1.4  val parse_type_arg_constrained =
     1.5    Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
     1.6  
     1.7 -val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained
     1.8 +val parse_type_arg_named_constrained =
     1.9 +  parse_opt_binding_colon Binding.empty -- parse_type_arg_constrained
    1.10  
    1.11  val parse_type_args_named_constrained =
    1.12    parse_type_arg_constrained >> (single o pair Binding.empty) ||
    1.13 @@ -1248,7 +1249,7 @@
    1.14    Scan.succeed no_map_rel;
    1.15  
    1.16  val parse_ctr_spec =
    1.17 -  parse_opt_binding_colon -- Parse.binding -- Scan.repeat parse_ctr_arg --
    1.18 +  parse_opt_binding_colon smart_binding -- Parse.binding -- Scan.repeat parse_ctr_arg --
    1.19    Scan.optional parse_defaults [] -- Parse.opt_mixfix;
    1.20  
    1.21  val parse_spec =