src/HOL/Tools/Predicate_Compile/core_data.ML

     fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
       let
         fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
         fun inst_of_matches tts =
           fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
-          |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of thy) o term_pair_of)
+          |> snd |> Vartab.dest |> map (apply2 (Thm.global_cterm_of thy) o term_pair_of)
         val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
         val case_th =
           rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
         val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1
         val pats =