src/Tools/Code/code_preproc.ML

     val (postproc, ct') = sandwich ctxt ct;
   in postproc (conv ctxt (Thm.term_of ct') ct') end;
 
 fun evaluation sandwich lift_postproc eval ctxt t =
   let
-    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     val (postproc, ct') = sandwich ctxt (cert t);
   in
     Thm.term_of ct'
     |> eval ctxt
     |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o cert)

 
 (* post- and preprocessing *)
 
 fun normalized_tfrees_sandwich ctxt ct =
   let
-    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     val t = Thm.term_of ct;
     val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
     val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
     val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));

   end;
 
 fun no_variables_sandwich ctxt ct =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
+    val cert = Thm.global_cterm_of thy;
     val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
       | t as Var _ => insert (op aconvc) (cert t)
       | _ => I) (Thm.term_of ct) [];
     fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
       |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))