# HG changeset patch
# User wenzelm
# Date 1517404839 -3600
# Node ID a965ccf7414e2f4deef60dbe75dcd32a959b5e61
# Parent  5f86e2a9c59c75156fa5ed6f9af084c46a14c7c4
performance fine-tuning of hot spot;

diff -r 5f86e2a9c59c -r a965ccf7414e src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Jan 31 14:11:57 2018 +0100
+++ b/src/Pure/General/table.ML	Wed Jan 31 14:20:39 2018 +0100
@@ -170,6 +170,25 @@
 
 (* lookup *)
 
+fun lookup tab key =
+  let
+    fun look Empty = NONE
+      | look (Branch2 (left, (k, x), right)) =
+          (case Key.ord (key, k) of
+            LESS => look left
+          | EQUAL => SOME x
+          | GREATER => look right)
+      | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+          (case Key.ord (key, k1) of
+            LESS => look left
+          | EQUAL => SOME x1
+          | GREATER =>
+              (case Key.ord (key, k2) of
+                LESS => look mid
+              | EQUAL => SOME x2
+              | GREATER => look right));
+  in look tab end;
+
 fun lookup_key tab key =
   let
     fun look Empty = NONE
@@ -189,8 +208,6 @@
               | GREATER => look right));
   in look tab end;
 
-fun lookup tab key = Option.map #2 (lookup_key tab key);
-
 fun defined tab key =
   let
     fun def Empty = false