src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -62,8 +62,8 @@
 
 fun mk_nat_thm thy t =
   let
-    val cn = Thm.cterm_of thy (Var (("n", 0), HOLogic.natT))
-    and ct = Thm.cterm_of thy t
+    val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT))
+    and ct = Thm.global_cterm_of thy t
   in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
 
 end;