src/HOL/Tools/inductive.ML

       error (Pretty.string_of (Pretty.block
         [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
 
     val elims = Induct.find_casesP ctxt prop;
 
-    val cprop = Thm.cterm_of thy prop;
+    val cprop = Thm.global_cterm_of thy prop;
     fun mk_elim rl =
       Thm.implies_intr cprop
         (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
       |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
   in

       (case substs of
         [s] => s
       | _ => error
         ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
     val inst =
-      map (fn v => (Thm.cterm_of thy (Var v), Thm.cterm_of thy (Envir.subst_term subst (Var v))))
+      map (fn v => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy (Envir.subst_term subst (Var v))))
         (Term.add_vars (lhs_of eq) []);
   in
     Drule.cterm_instantiate inst eq
     |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt)))
     |> singleton (Variable.export ctxt' ctxt)

            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> is_auxiliary ? Local_Theory.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
-        (Proof_Context.cterm_of lthy' (list_comb (rec_const, params)));
+        (Thm.cterm_of lthy' (list_comb (rec_const, params)));
     val specs =
       if length cs < 2 then []
       else
         map_index (fn (i, (name_mx, c)) =>
           let