--- 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 }