src/HOL/Tools/TFL/dcterm.ML

 
 (*---------------------------------------------------------------------------
  * Some simple constructor functions.
  *---------------------------------------------------------------------------*)
 
-val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
+val mk_hol_const = Thm.global_cterm_of @{theory HOL} o Const;
 
 fun mk_exists (r as (Bvar, Body)) =
   let val ty = Thm.typ_of_cterm Bvar
       val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
   in capply c (uncurry cabs r) end;

   let
     val thy = Thm.theory_of_cterm ctm;
     val t = Thm.term_of ctm;
   in
     if can HOLogic.dest_Trueprop t then ctm
-    else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
+    else Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
   end
   handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
     | TERM (msg, _) => raise ERR "mk_prop" msg;
 
 fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm;