--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 21:51:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 23:09:08 2012 +0200
@@ -9,8 +9,8 @@
signature BNF_GFP =
sig
- val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
- (term list * term list * thm list * thm list * thm list) * local_theory
+ val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
+ local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
end;
structure BNF_GFP : BNF_GFP =
@@ -52,7 +52,7 @@
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
(*all bnfs have the same lives*)
-fun bnf_gfp bs Dss_insts bnfs lthy =
+fun bnf_gfp bs resDs Dss_insts bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -66,7 +66,7 @@
(* TODO: check if m, n etc are sane *)
val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
- val deads = distinct (op =) (flat Dss);
+ val deads = fold (union (op =)) Dss (map TFree resDs);
val names_lthy = fold Variable.declare_typ deads lthy;
(* tvars *)
@@ -2950,7 +2950,7 @@
val Jbnf_notes =
[(map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
- (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
+ (set_set_inclN, map flat set_set_incl_thmsss),
(rel_unfoldN, map single Jrel_unfold_thms),
(pred_unfoldN, map single Jpred_unfold_thms)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss