src/HOL/Tools/Function/function_core.ML

 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   let
     val Globals {h, ...} = globals
 
     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
+    val cert = Proof_Context.cterm_of ctxt
 
     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
     val lGI = GIntro_thm
       |> Thm.forall_elim (cert f)
       |> fold Thm.forall_elim cqs

           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val cert = cterm_of (Proof_Context.theory_of lthy)
+    val cert = Proof_Context.cterm_of lthy
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
         val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
         val vars = Term.add_vars (prop_of thm) []

       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), dom) lthy
 
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
 
-    val cert = cterm_of (Proof_Context.theory_of lthy)
+    val cert = Proof_Context.cterm_of lthy
 
     val xclauses = PROFILE "xclauses"
       (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
         RCss GIntro_thms) RIntro_thmss