src/HOL/Nominal/nominal_fresh_fun.ML

     val Ts = map snd ps;
     val tinst' = map (fn (t, u) =>
       (head_of (Logic.incr_indexes (Ts, j) t),
        fold_rev Term.abs ps u)) tinst;
     val th' = instf
-      (map (apply2 (Thm.ctyp_of thy)) tyinst')
-      (map (apply2 (Thm.cterm_of thy)) tinst')
+      (map (apply2 (Thm.global_ctyp_of thy)) tyinst')
+      (map (apply2 (Thm.global_cterm_of thy)) tinst')
       (Thm.lift_rule cgoal th)
   in
     compose_tac ctxt (elim, th', Thm.nprems_of th) i st
   end handle General.Subscript => Seq.empty;
 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)

     fun inst_fresh vars params i st =
    let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
        val thy = Thm.theory_of_thm st;
    in case subtract (op =) vars vars' of
      [x] =>
-      Seq.single (Thm.instantiate ([], [(Thm.cterm_of thy x, Thm.cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
+      Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
     | _ => error "fresh_fun_simp: Too many variables, please report."
    end
   in
   ((fn st =>
   let