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/Tools/Metis/metis.ML
changeset 24133 75063f96618f
parent 23510 4521fead5609
child 24138 bd3fc8ff6bc9 
--- a/src/Tools/Metis/metis.ML	Thu Aug 02 21:43:55 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Thu Aug 02 21:45:07 2007 +0200
@@ -5386,7 +5386,7 @@
     | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
     | range (SOME i) (SOME j) =
     "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
-  fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true;
+  fun oLeq (SOME (x:int)) (SOME y) = x <= y | oLeq _ _ = true;
   fun argToInt arg omin omax x =
     (case Int.fromString x of
        SOME i =>
isabelle