# HG changeset patch
# User wenzelm
# Date 1116408660 -7200
# Node ID 48ae07a95c70bf18b5e6e696d961913e96af5734
# Parent  e0557c4521386be2638a4167b5bf8e87c3f492e0
removed update_node, which is just an instance of map_node;
tuned;

diff -r e0557c452138 -r 48ae07a95c70 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed May 18 11:30:59 2005 +0200
+++ b/src/Pure/General/graph.ML	Wed May 18 11:31:00 2005 +0200
@@ -27,7 +27,6 @@
   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                              (*exception DUP*)
-  val update_node : key * 'a -> 'a T -> 'a T
   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T
@@ -64,7 +63,7 @@
 val empty_keys = Table.empty: keys;
 
 infix mem_keys;
-fun x mem_keys tab = isSome (Table.lookup (tab: keys, x));
+fun x mem_keys tab = is_some (Table.lookup (tab: keys, x));
 
 infix ins_keys;
 fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
@@ -146,11 +145,6 @@
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new ((x, (info, ([], []))), tab));
 
-fun update_node (x, info) (G as Graph tab) =
-    let val (_, (preds, succs)) = get_entry G x in
-      Graph (Table.update ((x, (info, (preds, succs))), tab))
-    end;
-
 fun del_nodes xs (Graph tab) =
   Graph (tab
     |> fold Table.delete xs