--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Mar 06 15:58:56 2015 +0100
@@ -146,7 +146,7 @@
(* patterns and instantiations *)
fun mk_const_pat thy name destT =
- let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
+ let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
in (destT (Thm.ctyp_of_cterm cpat), cpat) end
val destT1 = hd o Thm.dest_ctyp
@@ -175,7 +175,7 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop})
+val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
fun dest_cprop ct =
(case Thm.term_of ct of