src/Pure/Isar/expression.ML

     val t = Logic.mk_conjunction_balanced ts;
     val body = Object_Logic.atomize_term thy t;
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT
-    then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
-    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
+    then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
+    else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
 
 fun aprop_tr' n c =

       (fn {context = ctxt, ...} =>
         rewrite_goals_tac ctxt [pred_def] THEN
         compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
         compose_tac defs_ctxt
           (false,
-            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_thy) norm_ts), 0) 1);
+            Conjunction.intr_balanced (map (Thm.assume o Thm.global_cterm_of defs_thy) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
-        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_thy statement))])
+        [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.global_cterm_of defs_thy statement))])
       |> Conjunction.elim_balanced (length ts);
 
     val (_, axioms_ctxt) = defs_ctxt
       |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>

 (* main predicate definition function *)
 
 fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val defs' = map (Thm.cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
+    val defs' = map (Thm.global_cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
 
     val (a_pred, a_intro, a_axioms, thy'') =
       if null exts then (NONE, NONE, [], thy)
       else
         let

       |> apfst (curry Notes "")
   | assumes_to_notes e axms = (e, axms);
 
 fun defines_to_notes ctxt (Defines defs) =
       Notes ("", map (fn (a, (def, _)) =>
-        (a, [([Assumption.assume ctxt (Proof_Context.cterm_of ctxt def)],
+        (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
 fun is_hyp (elem as Assumes asms) = true
   | is_hyp (elem as Defines defs) = true

     val hyp_spec = filter is_hyp body_elems;
 
     val notes =
       if is_some asm then
         [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
-          [([Assumption.assume pred_ctxt (Thm.cterm_of thy' (the asm))],
+          [([Assumption.assume pred_ctxt (Thm.global_cterm_of thy' (the asm))],
             [(Attrib.internal o K) Locale.witness_add])])])]
       else [];
 
     val notes' =
       body_elems