improved correctness of get_first (boundary check);
authorwenzelm
Sun, 14 Jun 2009 03:02:25 +0200
changeset 31621 924f3169ed62
parent 31620 b0f6168d2b25
child 31627 bc2de3795756
improved correctness of get_first (boundary check);
src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Jun 14 02:38:09 2009 +0200
+++ b/src/Pure/General/table.ML	Sun Jun 14 03:02:25 2009 +0200
@@ -137,7 +137,7 @@
     val check =
       (case boundary of
         NONE => K true
-      | SOME b => (fn k => Key.ord (b, k) = GREATER));
+      | SOME b => (fn k => Key.ord (b, k) = LESS));
     fun apply (k, x) = if check k then f (k, x) else NONE;
     fun get_bounded tb k = if check k then get tb else NONE
     and get Empty = NONE