src/HOL/Tools/BNF/bnf_def.ML

               let
                 val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As';
                 val funTs = map (fn T => bdT --> T) ranTs;
                 val ran_bnfT = mk_bnf_T ranTs Calpha;
                 val (revTs, Ts) = `rev (bd_bnfT :: funTs);
-                val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
+                val cTs = map (SOME o Proof_Context.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
                 val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
                   (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
                     map Bound (live - 1 downto 0)) $ Bound live));
-                val cts = [NONE, SOME (certify lthy tinst)];
+                val cts = [NONE, SOME (Proof_Context.cterm_of lthy tinst)];
               in
                 Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
               end);
             val bd = mk_cexp
               (if live = 0 then ctwo

         val in_rel = Lazy.lazy mk_in_rel;
 
         fun mk_rel_flip () =
           let
             val rel_conversep_thm = Lazy.force rel_conversep;
-            val cts = map (SOME o certify lthy) Rs;
+            val cts = map (SOME o Proof_Context.cterm_of lthy) Rs;
             val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
           in
             unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
             |> singleton (Proof_Context.export names_lthy pre_names_lthy)
           end;