src/HOL/Tools/SMT/smt_real.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59632 5980e75a204e
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -64,14 +64,14 @@
     1.4    fun mk_nary _ cu [] = cu
     1.5      | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
     1.6  
     1.7 -  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
     1.8 -  val add = Thm.cterm_of @{theory} @{const plus (real)}
     1.9 +  val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)})
    1.10 +  val add = Thm.global_cterm_of @{theory} @{const plus (real)}
    1.11    val real0 = Numeral.mk_cnumber @{ctyp real} 0
    1.12 -  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    1.13 -  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    1.14 -  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    1.15 -  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    1.16 -  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.17 +  val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)})
    1.18 +  val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)})
    1.19 +  val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)})
    1.20 +  val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)})
    1.21 +  val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)})
    1.22  
    1.23    fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.24      | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)