diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_smt_solver.ML
--- 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 }