src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51790 22517d04d20b
parent 51788 5fe72280a49f
child 51793 22f22172a361
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:47 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 12:09:51 2013 +0200
     1.3 @@ -1222,17 +1222,16 @@
     1.4    @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
     1.5  
     1.6  val parse_type_arg_constrained =
     1.7 -  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)
     1.8 +  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
     1.9  
    1.10 -val parse_type_arg_named_constrained =
    1.11 -  parse_opt_binding_colon Binding.empty -- parse_type_arg_constrained
    1.12 +val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
    1.13  
    1.14  val parse_type_args_named_constrained =
    1.15    parse_type_arg_constrained >> (single o pair Binding.empty) ||
    1.16    @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    1.17    Scan.succeed [];
    1.18  
    1.19 -val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
    1.20 +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
    1.21  
    1.22  val no_map_rel = (Binding.empty, Binding.empty);
    1.23  
    1.24 @@ -1249,11 +1248,11 @@
    1.25    Scan.succeed no_map_rel;
    1.26  
    1.27  val parse_ctr_spec =
    1.28 -  parse_opt_binding_colon smart_binding -- Parse.binding -- Scan.repeat parse_ctr_arg --
    1.29 +  parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
    1.30    Scan.optional parse_defaults [] -- Parse.opt_mixfix;
    1.31  
    1.32  val parse_spec =
    1.33 -  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
    1.34 +  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
    1.35    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    1.36  
    1.37  val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;