src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49134 846264f80f16
parent 49128 1a86ef0a0210
child 49169 937a0fadddfb
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 21:51:31 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 23:09:08 2012 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  signature BNF_GFP =
     1.6  sig
     1.7 -  val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
     1.8 -    (term list * term list * thm list * thm list * thm list) * local_theory
     1.9 +  val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
    1.10 +    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
    1.11  end;
    1.12  
    1.13  structure BNF_GFP : BNF_GFP =
    1.14 @@ -52,7 +52,7 @@
    1.15       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    1.16  
    1.17  (*all bnfs have the same lives*)
    1.18 -fun bnf_gfp bs Dss_insts bnfs lthy =
    1.19 +fun bnf_gfp bs resDs Dss_insts bnfs lthy =
    1.20    let
    1.21      val timer = time (Timer.startRealTimer ());
    1.22  
    1.23 @@ -66,7 +66,7 @@
    1.24      (* TODO: check if m, n etc are sane *)
    1.25  
    1.26      val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
    1.27 -    val deads = distinct (op =) (flat Dss);
    1.28 +    val deads = fold (union (op =)) Dss (map TFree resDs);
    1.29      val names_lthy = fold Variable.declare_typ deads lthy;
    1.30  
    1.31      (* tvars *)
    1.32 @@ -2950,7 +2950,7 @@
    1.33          val Jbnf_notes =
    1.34            [(map_simpsN, map single folded_map_simp_thms),
    1.35            (set_inclN, set_incl_thmss),
    1.36 -          (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
    1.37 +          (set_set_inclN, map flat set_set_incl_thmsss),
    1.38            (rel_unfoldN, map single Jrel_unfold_thms),
    1.39            (pred_unfoldN, map single Jpred_unfold_thms)] @
    1.40            map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss