diff -r e776a4b813d1 -r ee270328a781 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:19 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -207,7 +207,7 @@
             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
             |> funpow n (fn thm => thm RS spec)
             |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
-            |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
+            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
                Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
                maps mk_fp_type_copy_thms fp_type_definitions @
                maps mk_type_copy_thms type_definitions)