Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/Arith/fast_lin_arith.ML
changeset 77879 dd222e2af01a
parent 74561 8e6c973003c8
child 78133 0a098088745b 
--- 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
isabelle