--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Mar 06 23:52:35 2015 +0100
@@ -30,7 +30,7 @@
local
val (cpfalse, cfalse) =
- `Old_SMT_Utils.mk_cprop (Thm.global_cterm_of @{theory} @{const False})
+ `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False})
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -203,8 +203,7 @@
Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1
fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct
- fun mk_clist T = apply2 (Thm.global_cterm_of @{theory})
- (HOLogic.cons_const T, HOLogic.nil_const T)
+ fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T)
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
val mk_pat_list = mk_list (mk_clist @{typ pattern})
val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"})
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Fri Mar 06 23:52:35 2015 +0100
@@ -64,14 +64,14 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
- val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)})
- val add = Thm.global_cterm_of @{theory} @{const plus (real)}
+ val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)})
+ val add = Thm.cterm_of @{context} @{const plus (real)}
val real0 = Numeral.mk_cnumber @{ctyp real} 0
- val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)})
- val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)})
- val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)})
- val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)})
- val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)})
+ val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)})
+ val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)})
+ val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)})
+ val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)})
+ val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)})
fun z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("+", _)) cts =
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Mar 06 23:52:35 2015 +0100
@@ -195,7 +195,7 @@
const_defs = us})
end)
- val cfalse = Thm.global_cterm_of @{theory} (@{const Trueprop} $ @{const False})
+ val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False})
in
fun add_solver cfg =
@@ -268,7 +268,7 @@
(* filter *)
-val cnot = Thm.global_cterm_of @{theory} @{const Not}
+val cnot = Thm.cterm_of @{context} @{const Not}
fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Mar 06 23:52:35 2015 +0100
@@ -175,7 +175,7 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
+val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
fun dest_cprop ct =
(case Thm.term_of ct of
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML Fri Mar 06 23:52:35 2015 +0100
@@ -137,13 +137,13 @@
| mk_builtin_num ctxt i T =
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
-val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
-val mk_false = Thm.global_cterm_of @{theory} @{const False}
-val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
-val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
-val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
-val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
-val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
+val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{context} @{const False}
+val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{context} @{const HOL.conj}
+val disj = Thm.cterm_of @{context} @{const HOL.disj}
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -184,15 +184,15 @@
Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value
end
-val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
-val add = Thm.global_cterm_of @{theory} @{const plus (int)}
+val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
+val add = Thm.cterm_of @{context} @{const plus (int)}
val int0 = Numeral.mk_cnumber @{ctyp int} 0
-val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
-val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
-val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
--- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Mar 06 23:52:35 2015 +0100
@@ -82,7 +82,7 @@
| NONE => false)
in exists end
-val negate = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
+val negate = Thm.apply (Thm.cterm_of @{context} @{const Not})
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Mar 06 23:52:35 2015 +0100
@@ -181,7 +181,7 @@
(** parser context **)
-val not_false = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
+val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False})
fun make_context ctxt typs terms =
let
@@ -381,7 +381,7 @@
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
-val ctrue = Thm.global_cterm_of @{theory} @{const True}
+val ctrue = Thm.cterm_of @{context} @{const True}
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
(the o mk_fun (K (SOME ctrue)))) st
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Mar 06 23:52:35 2015 +0100
@@ -229,7 +229,7 @@
| _ => fresh_abstraction dcvs ct cx)))
in abstr (depth, []) end
-val cimp = Thm.global_cterm_of @{theory} @{const Pure.imp}
+val cimp = Thm.cterm_of @{context} @{const Pure.imp}
fun deepen depth f x =
if depth = 0 then f depth x