# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID ce8297d5017aa7f6bae7b6f53b474b7f94701a0c
# Parent  360a05d6076159d185cf100e38dd2b7c140de821
pick up all 'nesting' theorems

diff -r 360a05d60761 -r ce8297d5017a src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -72,8 +72,8 @@
   IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
 
 fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
-        fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs, ...}
-      : fp_sugar) :: _) thy =
+      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
+      nesting_bnfs, ...} : fp_sugar) :: _) thy =
     let
       val data = Data.get thy;
 
@@ -200,7 +200,7 @@
         map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
 
       val nested_size_maps = map (pointfill thy3_ctxt) nested_size_o_maps @ nested_size_o_maps;
-      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs);
+      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
 
       fun derive_size_simp size_def' simp0 =
         (trans OF [size_def', simp0])