# HG changeset patch
# User obua
# Date 1093362924 -7200
# Node ID 394fb9b8908b4de2f18f18573c5e40ee31c1a46f
# Parent  2ef19a680646d157c0bb5c44421c04713d2e86c0
changes

diff -r 2ef19a680646 -r 394fb9b8908b src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Mon Aug 23 18:35:11 2004 +0200
+++ b/src/Pure/General/graph.ML	Tue Aug 24 17:55:24 2004 +0200
@@ -18,7 +18,7 @@
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
-  val get_node: 'a T -> key -> 'a
+  val get_node: 'a T -> key -> 'a (* UNDEF *)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val imm_preds: 'a T -> key -> key list
   val imm_succs: 'a T -> key -> key list
@@ -26,7 +26,7 @@
   val all_succs: 'a T -> key list -> key list
   val strong_conn: 'a T -> key list list
   val find_paths: 'a T -> key * key -> key list list
-  val new_node: key * 'a -> 'a T -> 'a T
+  val new_node: key * 'a -> 'a T -> 'a T (* DUP *)
   val del_nodes: key list -> 'a T -> 'a T
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T
diff -r 2ef19a680646 -r 394fb9b8908b src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Aug 23 18:35:11 2004 +0200
+++ b/src/Pure/General/table.ML	Tue Aug 24 17:55:24 2004 +0200
@@ -26,6 +26,7 @@
   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 exists: (key * 'a -> bool) -> 'a table -> bool
   val lookup: 'a table * key -> 'a option
   val update: (key * 'a) * 'a table -> 'a table
@@ -92,6 +93,9 @@
   | min_key (Branch2 (left, (k, _), _)) = Some (if_none (min_key left) k)
   | min_key (Branch3 (left, (k, _), _, _, _)) = Some (if_none (min_key left) k);
 
+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);
 
 (* lookup *)