src/HOL/Tools/TFL/dcterm.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59640 a6d29266f01c
     1.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4   * Some simple constructor functions.
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 -val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
     1.8 +val mk_hol_const = Thm.global_cterm_of @{theory HOL} o Const;
     1.9  
    1.10  fun mk_exists (r as (Bvar, Body)) =
    1.11    let val ty = Thm.typ_of_cterm Bvar
    1.12 @@ -181,7 +181,7 @@
    1.13      val t = Thm.term_of ctm;
    1.14    in
    1.15      if can HOLogic.dest_Trueprop t then ctm
    1.16 -    else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
    1.17 +    else Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
    1.18    end
    1.19    handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
    1.20      | TERM (msg, _) => raise ERR "mk_prop" msg;