--- 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;