src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49169 937a0fadddfb
parent 49134 846264f80f16
child 49176 6d29d2db5f88
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 19:57:50 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 19:58:09 2012 +0200
     1.3 @@ -9,8 +9,9 @@
     1.4  
     1.5  signature BNF_GFP =
     1.6  sig
     1.7 -  val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
     1.8 -    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
     1.9 +  val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
    1.10 +    BNF_Def.BNF list -> local_theory ->
    1.11 +    (term list * term list * thm list * thm list * thm list) * local_theory
    1.12  end;
    1.13  
    1.14  structure BNF_GFP : BNF_GFP =
    1.15 @@ -52,7 +53,7 @@
    1.16       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    1.17  
    1.18  (*all bnfs have the same lives*)
    1.19 -fun bnf_gfp bs resDs Dss_insts bnfs lthy =
    1.20 +fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
    1.21    let
    1.22      val timer = time (Timer.startRealTimer ());
    1.23  
    1.24 @@ -1830,9 +1831,9 @@
    1.25  
    1.26      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
    1.27        lthy
    1.28 -      |> fold_map3 (fn b => fn car_final => fn in_car_final =>
    1.29 -        typedef false NONE (b, params, NoSyn) car_final NONE
    1.30 -          (EVERY' [rtac exI, rtac in_car_final] 1)) bs car_finals in_car_final_thms
    1.31 +      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
    1.32 +        typedef false NONE (b, params, mx) car_final NONE
    1.33 +          (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
    1.34        |>> apsnd split_list o split_list;
    1.35  
    1.36      val Ts = map (fn name => Type (name, params')) T_names;