diff -r 35a1788dd6f9 -r dd222e2af01a src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -437,7 +437,7 @@
             val T = Thm.typ_of_cterm cv
           in
             mth
-            |> Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), number_of T n)])
+            |> Thm.instantiate (TVars.empty, Vars.make1 (dest_Var (Thm.term_of cv), number_of T n))
             |> rewrite_concl
             |> discharge_prem
             handle CTERM _ => mult_by_add n thm