src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51757 7babcb61aa5c
parent 51756 b0bae7bd236c
child 51758 55963309557b
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 13:16:20 2013 +0200
     1.3 @@ -8,14 +8,16 @@
     1.4  signature BNF_FP_DEF_SUGAR =
     1.5  sig
     1.6    val datatypes: bool ->
     1.7 -    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
     1.8 -      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
     1.9 +    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
    1.10 +      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.11 +      BNF_FP.fp_result * local_theory) ->
    1.12      (bool * bool) * (((((binding * typ) * sort) list * binding) * mixfix) * ((((binding * binding) *
    1.13        (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    1.14      local_theory -> local_theory
    1.15    val parse_datatype_cmd: bool ->
    1.16 -    (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    1.17 -      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
    1.18 +    (mixfix list -> (string * sort) list option -> binding list -> binding list list ->
    1.19 +      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.20 +      BNF_FP.fp_result * local_theory) ->
    1.21      (local_theory -> local_theory) parser
    1.22  end;
    1.23  
    1.24 @@ -163,6 +165,7 @@
    1.25      val Ass0 = map (map prepare_type_arg o type_args_constrained_of) specs;
    1.26      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    1.27      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    1.28 +    val set_bss = map (map (fst o fst) o type_args_constrained_of) specs;
    1.29  
    1.30      val (((Bs0, Cs), Xs), no_defs_lthy) =
    1.31        no_defs_lthy0
    1.32 @@ -237,7 +240,7 @@
    1.33      val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
    1.34             fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    1.35             fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    1.36 -      fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.37 +      fp_bnf construct_fp fp_bs mixfixes set_bss (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.38  
    1.39      val timer = time (Timer.startRealTimer ());
    1.40