# HG changeset patch
# User blanchet
# Date 1400237799 -7200
# Node ID 0c1b4987e6b288a32107e6d90ab8f792cae646f4
# Parent  a33fe940a557a51772587b2f7cd2c2a6e554b626
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')

diff -r a33fe940a557 -r 0c1b4987e6b2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri May 16 09:19:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri May 16 12:56:39 2014 +0200
@@ -1146,10 +1146,11 @@
               fun mk_map_thm ctr_def' cxIn =
                 fold_thms lthy [ctr_def']
                   (unfold_thms lthy (o_apply :: pre_map_def ::
-                       (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sumprod_thms_map @
+                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @
                        abs_inverses)
                      (cterm_instantiate_pos (nones @ [SOME cxIn])
-                        (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
+                        (if fp = Least_FP then fp_map_thm
+                         else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);
 
               fun mk_set_thm fp_set_thm ctr_def' cxIn =