# HG changeset patch
# User berghofe
# Date 952696832 -3600
# Node ID ef01ee11b14ea8757a937a2efeca60a87cb39334
# Parent  4d981311dab7b5f9b0de2f11d8c711792302b524
Added function min_key.

diff -r 4d981311dab7 -r ef01ee11b14e src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Mar 10 15:00:01 2000 +0100
+++ b/src/Pure/General/table.ML	Fri Mar 10 15:00:32 2000 +0100
@@ -24,6 +24,7 @@
   val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
+  val min_key: 'a table -> key option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val lookup: 'a table * key -> 'a option
   val update: (key * 'a) * 'a table -> 'a table
@@ -79,6 +80,10 @@
 fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
 fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
 
+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);
+
 
 (* lookup *)