--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 00:21:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200
@@ -66,12 +66,12 @@
val rec_o_map_simp_thms =
@{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
+fun mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
- HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @
- rec_o_map_simp_thms) ctxt));
+ HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
+ distinct Thm.eq_thm_prop (nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
@@ -258,6 +258,7 @@
let
val pre_bnfs = map #pre_bnf fp_sugars;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ val nesting_map_idents = map map_ident_of_bnf nesting_bnfs;
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
val rec_defs = map #co_rec_def fp_sugars;
@@ -302,7 +303,8 @@
val rec_o_map_thms =
map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map)
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs nesting_map_idents abs_inverses
+ ctor_rec_o_map)
|> Thm.close_derivation)
rec_o_map_goals rec_defs ctor_rec_o_maps;