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/HOL/Tools/semiring_normalizer.ML
changeset 77879 dd222e2af01a
parent 74561 8e6c973003c8
child 78095 bc42c074e58f 
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -144,7 +144,7 @@
       in if b = 1 then Numeral.mk_cnumber cT a
         else Thm.apply
              (Thm.apply
-               (Thm.instantiate_cterm (TVars.make [(divide_tvar, cT)], Vars.empty) divide_const)
+               (Thm.instantiate_cterm (TVars.make1 (divide_tvar, cT), Vars.empty) divide_const)
                (Numeral.mk_cnumber cT a))
              (Numeral.mk_cnumber cT b)
       end
isabelle