# HG changeset patch
# User wenzelm
# Date 1121435059 -7200
# Node ID 0f536ece46e352b953101488ebc8dbc4cf514e58
# Parent  79b9a6481ae450d7abaa27b4b9203d23b3612731
tuned min_key, max_key;

diff -r 79b9a6481ae4 -r 0f536ece46e3 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Jul 15 15:44:18 2005 +0200
+++ b/src/Pure/General/table.ML	Fri Jul 15 15:44:19 2005 +0200
@@ -115,12 +115,16 @@
 end;
 
 fun min_key Empty = NONE
-  | min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)
-  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (if_none (min_key left) k);
+  | min_key (Branch2 (Empty, (k, _), _)) = SOME k
+  | min_key (Branch3 (Empty, (k, _), _, _, _)) = SOME k
+  | min_key (Branch2 (left, _, _)) = min_key left
+  | min_key (Branch3 (left, _, _, _, _)) = min_key left;
 
 fun max_key Empty = NONE
-  | max_key (Branch2 (_, (k, _), right)) = SOME (if_none (max_key right) k)
-  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (if_none (max_key right) k);
+  | max_key (Branch2 (_, (k, _), Empty)) = SOME k
+  | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k
+  | max_key (Branch2 (_, _, right)) = max_key right
+  | max_key (Branch3 (_, _, _, _, right)) = max_key right;
 
 
 (* lookup *)