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 60642 48dd1cefb4ae
parent 60348 e66830e878e3
child 61097 93f08a05abc9 
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -424,7 +424,7 @@
             val T = Thm.typ_of_cterm cv
           in
             mth
-            |> Thm.instantiate ([], [(cv, number_of T n)])
+            |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)])
             |> rewrite_concl
             |> discharge_prem
             handle CTERM _ => mult_by_add n thm
isabelle