src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 59580 cbc38731d42f
parent 59058 a78612c67ec0
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 03 17:20:51 2015 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 03 19:08:04 2015 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4            case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
     1.5          val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
     1.6          val thetas = AList.group (op =)
     1.7 -          (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis));
     1.8 +          (mutual_cliques ~~ map (apply2 (Proof_Context.cterm_of lthy)) (raw_phis ~~ pre_phis));
     1.9        in
    1.10          map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
    1.11          mutual_cliques rel_xtor_co_inducts
    1.12 @@ -214,7 +214,7 @@
    1.13              fun mk_Grp_id P =
    1.14                let val T = domain_type (fastype_of P);
    1.15                in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
    1.16 -            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
    1.17 +            val cts = map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
    1.18              fun mk_fp_type_copy_thms thm = map (curry op RS thm)
    1.19                @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
    1.20              fun mk_type_copy_thms thm = map (curry op RS thm)
    1.21 @@ -235,7 +235,7 @@
    1.22            end
    1.23        | Greatest_FP =>
    1.24            let
    1.25 -            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
    1.26 +            val cts = NONE :: map (SOME o Proof_Context.cterm_of lthy) (map HOLogic.eq_const As);
    1.27            in
    1.28              cterm_instantiate_pos cts xtor_rel_co_induct
    1.29              |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @