src/HOL/Tools/SMT/z3_interface.ML
changeset 59632 5980e75a204e
parent 59621 291934bac95e
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Mar 06 23:44:51 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Mar 06 23:44:57 2015 +0100
     1.3 @@ -112,13 +112,13 @@
     1.4    | mk_builtin_num ctxt i T =
     1.5        chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
     1.6  
     1.7 -val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
     1.8 -val mk_false = Thm.global_cterm_of @{theory} @{const False}
     1.9 -val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
    1.10 -val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
    1.11 -val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
    1.12 -val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
    1.13 -val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
    1.14 +val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
    1.15 +val mk_false = Thm.cterm_of @{context} @{const False}
    1.16 +val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
    1.17 +val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
    1.18 +val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
    1.19 +val conj = Thm.cterm_of @{context} @{const HOL.conj}
    1.20 +val disj = Thm.cterm_of @{context} @{const HOL.disj}
    1.21  
    1.22  fun mk_nary _ cu [] = cu
    1.23    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
    1.24 @@ -139,15 +139,15 @@
    1.25    let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
    1.26    in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
    1.27  
    1.28 -val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
    1.29 -val add = Thm.global_cterm_of @{theory} @{const plus (int)}
    1.30 +val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
    1.31 +val add = Thm.cterm_of @{context} @{const plus (int)}
    1.32  val int0 = Numeral.mk_cnumber @{ctyp int} 0
    1.33 -val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
    1.34 -val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
    1.35 -val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
    1.36 -val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
    1.37 -val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
    1.38 -val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
    1.39 +val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
    1.40 +val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
    1.41 +val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
    1.42 +val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
    1.43 +val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
    1.44 +val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
    1.45  
    1.46  fun mk_builtin_fun ctxt sym cts =
    1.47    (case (sym, cts) of