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 60801 7664e0916eec
parent 60642 48dd1cefb4ae
child 61075 f6b0d827240e 
--- a/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -142,7 +142,7 @@
       let val (a, b) = Rat.quotient_of_rat x
       in if b = 1 then Numeral.mk_cnumber cT a
         else Thm.apply
-             (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+             (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
                          (Numeral.mk_cnumber cT a))
              (Numeral.mk_cnumber cT b)
       end
isabelle