src/Pure/General/table.ML

   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
-  val min_key: 'a table -> key option
-  val max_key: 'a table -> key option
+  val min: 'a table -> (key * 'a) option
+  val max: 'a table -> (key * 'a) option
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
   val lookup_key: 'a table -> key -> (key * 'a) option
   val lookup: 'a table -> key -> 'a option

 
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
 
-(* min/max keys *)
-
-fun min_key Empty = NONE
-  | 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, _), Empty)) = SOME k
-  | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k
-  | max_key (Branch2 (_, _, right)) = max_key right
-  | max_key (Branch3 (_, _, _, _, right)) = max_key right;
+(* min/max entries *)
+
+fun min Empty = NONE
+  | min (Branch2 (Empty, p, _)) = SOME p
+  | min (Branch3 (Empty, p, _, _, _)) = SOME p
+  | min (Branch2 (left, _, _)) = min left
+  | min (Branch3 (left, _, _, _, _)) = min left;
+
+fun max Empty = NONE
+  | max (Branch2 (_, p, Empty)) = SOME p
+  | max (Branch3 (_, _, _, p, Empty)) = SOME p
+  | max (Branch2 (_, _, right)) = max right
+  | max (Branch3 (_, _, _, _, right)) = max right;
 
 
 (* get_first *)
 
 fun get_first f =