# HG changeset patch
# User wenzelm
# Date 1244941345 -7200
# Node ID 924f3169ed62bf4e7e641fc9ad769eabed26619b
# Parent  b0f6168d2b2552fed64482dde93135254b551bb6
improved correctness of get_first (boundary check);

diff -r b0f6168d2b25 -r 924f3169ed62 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