diff -r 165c97f9bb63 -r 5be3a21ec949 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Aug 24 12:07:00 2005 +0200
+++ b/src/Pure/General/graph.ML	Thu Aug 25 09:23:13 2005 +0200
@@ -27,6 +27,7 @@
   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 default_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
@@ -143,6 +144,9 @@
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new ((x, (info, ([], []))), tab));
 
+fun default_node x info (Graph tab) =
+  Graph (Table.default x (info, ([], [])) tab);
+
 fun del_nodes xs (Graph tab) =
   Graph (tab
     |> fold Table.delete xs