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/numeral_simprocs.ML
changeset 31101 26c7bb764a38
parent 31068 f591144b0f17
child 31368 763f4b0fd579 
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon May 11 15:57:29 2009 +0200
@@ -516,7 +516,7 @@
       val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
       fun prove p =
-        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
+        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)
isabelle