# HG changeset patch
# User blanchet
# Date 1403856704 -7200
# Node ID 465ac4021146507ebe1de50d033e636e1d00578d
# Parent  7621a3b42ce7e08a97028d9162479ebc795568f6
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side

diff -r 7621a3b42ce7 -r 465ac4021146 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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;