# 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])