diff -r 92d7d8e4f1bf -r 291934bac95e src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -483,7 +483,7 @@
     simplify_one ctxt (([th, cancel_th]) MRS trans);
 
 local
-  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
+  val Tp_Eq = Thm.reflexive (Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop)
   fun Eq_True_elim Eq = 
     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
 in
@@ -494,7 +494,7 @@
       val pos = less $ zero $ t and neg = less $ t $ zero
       val thy = Proof_Context.theory_of ctxt
       fun prove p =
-        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of thy p)))
+        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.global_cterm_of thy p)))
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)