src/HOL/Tools/coinduction.ML

             |> try (Library.foldr1 HOLogic.mk_conj)
             |> the_default @{term True}
             |> Ctr_Sugar_Util.list_exists_free vars
             |> Term.map_abs_vars (Variable.revert_fixed ctxt)
             |> fold_rev Term.absfree (names ~~ Ts)
-            |> Ctr_Sugar_Util.certify ctxt;
+            |> Proof_Context.cterm_of ctxt;
           val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
           val e = length eqs;
           val p = length prems;
         in
           HEADGOAL (EVERY' [resolve_tac ctxt [thm],
             EVERY' (map (fn var =>
               resolve_tac ctxt
                 [Ctr_Sugar_Util.cterm_instantiate_pos
-                  [NONE, SOME (Ctr_Sugar_Util.certify ctxt var)] exI]) vars),
+                  [NONE, SOME (Proof_Context.cterm_of ctxt var)] exI]) vars),
             if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
             else
               REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
               Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
             K (ALLGOALS_SKIP skip