1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 14 12:09:27 2012 +0200
1.3 @@ -175,17 +175,20 @@
1.4 fp_iter_thms, fp_rec_thms), lthy)) =
1.5 fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
1.6
1.7 - val add_nested_bnf_names =
1.8 + fun add_nesty_bnf_names Us =
1.9 let
1.10 fun add (Type (s, Ts)) ss =
1.11 let val (needs, ss') = fold_map add Ts ss in
1.12 if exists I needs then (true, insert (op =) s ss') else (false, ss')
1.13 end
1.14 - | add T ss = (member (op =) Bs T, ss);
1.15 + | add T ss = (member (op =) Us T, ss);
1.16 in snd oo add end;
1.17
1.18 - val nested_bnfs =
1.19 - map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssBs []);
1.20 + fun nesty_bnfs Us =
1.21 + map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssBs []);
1.22 +
1.23 + val nesting_bnfs = nesty_bnfs As;
1.24 + val nested_bnfs = nesty_bnfs Bs;
1.25
1.26 val timer = time (Timer.startRealTimer ());
1.27
1.28 @@ -498,7 +501,7 @@
1.29
1.30 val pre_map_defs = map map_def_of_bnf pre_bnfs;
1.31 val pre_set_defss = map set_defs_of_bnf pre_bnfs;
1.32 - val map_ids = map map_id_of_bnf nested_bnfs;
1.33 + val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
1.34
1.35 fun mk_map Ts Us t =
1.36 let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
1.37 @@ -626,9 +629,11 @@
1.38 val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
1.39
1.40 val iter_tacss =
1.41 - map2 (map o mk_iter_like_tac pre_map_defs map_ids iter_defs) fp_iter_thms ctr_defss;
1.42 + map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
1.43 + ctr_defss;
1.44 val rec_tacss =
1.45 - map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
1.46 + map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
1.47 + ctr_defss;
1.48 in
1.49 (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
1.50 goal_iterss iter_tacss,
1.51 @@ -704,10 +709,10 @@
1.52 map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss';
1.53
1.54 val coiter_tacss =
1.55 - map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
1.56 + map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
1.57 ctr_defss;
1.58 val corec_tacss =
1.59 - map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs
1.60 + map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
1.61 ctr_defss;
1.62 in
1.63 (map2 (map2 (fn goal => fn tac =>