src/HOL/BNF/Tools/bnf_fp_n2m.ML
changeset 54742 7a86358a3c0b
parent 54740 91f54d386680
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4              cterm_instantiate_pos cts rel_xtor_co_induct_thm
     1.5              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
     1.6              |> funpow (2 * n) (fn thm => thm RS spec)
     1.7 -            |> Conv.fconv_rule Object_Logic.atomize
     1.8 +            |> Conv.fconv_rule (Object_Logic.atomize lthy)
     1.9              |> funpow n (fn thm => thm RS mp)
    1.10            end);
    1.11