diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -60,8 +60,9 @@
 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 ([], [((("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 [((("n", 0), HOLogic.natT), ct)]) @{thm le0}
+  end;
 
 end;