src/Tools/Code/code_preproc.ML

    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
         val thy = Proof_Context.theory_of ctxt;
         val functrans = (map (fn (_, (_, f)) => f ctxt)
           o #functrans o the_thmproc) thy;
-        val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
+        val cert = Code.get_cert ctxt functrans c;
         val (lhs, rhss) =
           Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;
 
 fun obtain_instance ctxt arities (inst as (class, tyco)) =