src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55854 ee270328a781
parent 55819 e21d83c8e1c7
child 55868 37b99986d435
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:19 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4              |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
     1.5              |> funpow n (fn thm => thm RS spec)
     1.6              |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
     1.7 -            |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
     1.8 +            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
     1.9                 Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
    1.10                 maps mk_fp_type_copy_thms fp_type_definitions @
    1.11                 maps mk_type_copy_thms type_definitions)