src/Pure/Proof/proof_checker.ML

 
         fun thm_of_atom thm Ts =
           let
             val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
             val (fmap, thm') = Thm.varifyT_global' [] thm;
-            val ctye = map (apply2 (Thm.ctyp_of thy))
+            val ctye = map (apply2 (Thm.global_ctyp_of thy))
               (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
           in
             Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 

           | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
               let
                 val (x, names') = Name.variant s names;
                 val thm = thm_of ((x, T) :: vs, names') Hs prf
               in
-                Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
+                Thm.forall_intr (Thm.global_cterm_of thy (Free (x, T))) thm
               end
 
           | thm_of (vs, names) Hs (prf % SOME t) =
               let
                 val thm = thm_of (vs, names) Hs prf;
-                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+                val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
               in
                 Thm.forall_elim ct thm
                 handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
               end
 
           | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
               let
-                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+                val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
                 val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
               in
                 Thm.implies_intr ct thm
               end
 

               in
                 Thm.implies_elim thm thm'
                 handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
               end
 
-          | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
+          | thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
 
           | thm_of _ _ _ = error "thm_of_proof: partial proof term";
 
       in beta_eta_convert (thm_of ([], prf_names) [] prf) end
   end;