--- a/src/HOL/Tools/lin_arith.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sat Sep 11 13:04:32 2021 +0200
@@ -60,9 +60,8 @@
fun is_nat t = (fastype_of1 t = HOLogic.natT);
fun mk_nat_thm thy t =
- let val ct = Thm.global_cterm_of thy t in
- Drule.instantiate_normalize (TVars.empty, Vars.make [((("n", 0), HOLogic.natT), ct)]) @{thm le0}
- end;
+ let val ct = Thm.global_cterm_of thy t
+ in Drule.instantiate_normalize (TVars.empty, Vars.make [(\<^var>\<open>?n::nat\<close>, ct)]) @{thm le0} end;
end;