diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -60,10 +60,8 @@
 fun is_nat t = (fastype_of1 t = HOLogic.natT);
 
 fun mk_nat_thm thy t =
-  let
-    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;
+  let val ct = Thm.global_cterm_of thy t
+  in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end;
 
 end;