src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55699 1f9cc432ecd4
parent 55575 a5e33e18fb5c
child 55700 cf6a029b28d8
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 21:53:01 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4      local_theory -> gfp_sugar_thms
     1.5  
     1.6    type co_datatype_spec =
     1.7 -    ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
     1.8 +    ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
     1.9      * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
    1.10  
    1.11    val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    1.12 @@ -285,7 +285,7 @@
    1.13    handle THM _ => thm;
    1.14  
    1.15  type co_datatype_spec =
    1.16 -  ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    1.17 +  ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    1.18    * ((binding, binding * typ, term) ctr_spec * mixfix) list;
    1.19  
    1.20  fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
    1.21 @@ -972,7 +972,9 @@
    1.22      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    1.23      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    1.24      val num_As = length unsorted_As;
    1.25 -    val set_bss = map (map fst o type_args_named_constrained_of_spec) specs;
    1.26 +
    1.27 +    val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
    1.28 +    val set_bss = map (map (the_default Binding.empty)) set_boss;
    1.29  
    1.30      val (((Bs0, Cs), Xs), no_defs_lthy) =
    1.31        no_defs_lthy0
    1.32 @@ -1471,18 +1473,6 @@
    1.33  fun co_datatype_cmd x =
    1.34    define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
    1.35  
    1.36 -val parse_type_arg_constrained =
    1.37 -  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
    1.38 -
    1.39 -val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
    1.40 -
    1.41 -(*FIXME: use parse_type_args_named_constrained from BNF_Util and thus 
    1.42 -  allow users to kill certain arguments of a (co)datatype*)
    1.43 -val parse_type_args_named_constrained =
    1.44 -  parse_type_arg_constrained >> (single o pair Binding.empty) ||
    1.45 -  @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    1.46 -  Scan.succeed [];
    1.47 -
    1.48  val parse_ctr_arg =
    1.49    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
    1.50    (Parse.typ >> pair Binding.empty);