src/HOL/Tools/Transfer/transfer_bnf.ML

     val old_lthy = lthy
     val (As, lthy) = mk_TFrees' (sorts_of_fp fp_sugar) lthy
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy
     val args = map mk_eq_onp preds
-    val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
-    val cts = map (SOME o certify lthy) args
+    val cTs = map (SOME o Proof_Context.ctyp_of lthy) (maps (replicate 2) As)
+    val cts = map (SOME o Proof_Context.cterm_of lthy) args
     fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
     fun is_eqn thm = can get_rhs thm
     fun rel2pred_massage thm =
       let
         val live_step = @{lemma "x = y \<Longrightarrow> (eq_onp P a a \<and> x) = (P a \<and> y)" by (simp only: eq_onp_same_args)}