# HG changeset patch
# User blanchet
# Date 1394554722 -3600
# Node ID c6a15aa64e36c0ae153aa650eb2458fa3b56d41a
# Parent  d311c6377e08bb8865da4636fac6a887b34d086b
added missing theorems to unfolding set

diff -r d311c6377e08 -r c6a15aa64e36 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 11 17:18:41 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 11 17:18:42 2014 +0100
@@ -1222,7 +1222,7 @@
                 fold_thms lthy ctr_defs'
                   (unfold_thms lthy (pre_rel_def :: abs_inverse ::
                        (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
-                       @{thms vimage2p_def Inl_Inr_False})
+                       @{thms vimage2p_def sum.inject Inl_Inr_False})
                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
                 |> postproc
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);