src/HOL/Tools/BNF/bnf_lfp_size.ML

             val (xs, names_lthy2) = mk_Frees "x" (binder_types (fastype_of size)) lthy2;
             val goal =
               HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero);
             val thm =
               Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
-                mk_size_neq ctxt (map (certify lthy2) xs)
+                mk_size_neq ctxt (map (Proof_Context.cterm_of lthy2) xs)
                 (#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
               |> single
               |> Proof_Context.export names_lthy2 lthy2
               |> map Thm.close_derivation;
           in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss