# HG changeset patch
# User wenzelm
# Date 1244923293 -7200
# Node ID 2e4430b84303768df88e5654ea07dbb62200f71b
# Parent  bb7b5a5942c733ad13dca85615739c395c8110ea
improved get_first: check boundary before entering subtrees;

diff -r bb7b5a5942c7 -r 2e4430b84303 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Jun 13 19:40:37 2009 +0200
+++ b/src/Pure/General/table.ML	Sat Jun 13 22:01:33 2009 +0200
@@ -136,26 +136,26 @@
   let
     val check =
       (case boundary of
-        NONE => (fn p => f p)
-      | SOME b => (fn p as (k, _) =>
-          (case Key.ord (b, k) of GREATER => f p | _ => NONE)));
-
-    fun get Empty = NONE
-      | get (Branch2 (left, p, right)) =
-          (case get left of
+        NONE => K true
+      | SOME b => (fn k => Key.ord (b, k) = GREATER));
+    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
+      | get (Branch2 (left, (k, x), right)) =
+          (case get_bounded left k of
             NONE =>
-              (case check p of
+              (case apply (k, x) of
                 NONE => get right
               | some => some)
           | some => some)
-      | get (Branch3 (left, p, mid, q, right)) =
-          (case get left of
+      | get (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+          (case get_bounded left k1 of
             NONE =>
-              (case check p of
+              (case apply (k1, x1) of
                 NONE =>
-                  (case get mid of
+                  (case get_bounded mid k2 of
                     NONE =>
-                      (case check q of
+                      (case apply (k2, x2) of
                         NONE => get right
                       | some => some)
                   | some => some)