src/Pure/General/graph.ML

   val all_preds: 'a T -> key list -> key list
   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                              (*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
   val del_edge: key * key -> 'a T -> 'a T
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)

 (* nodes *)
 
 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
     |> Table.map (fn (i, (preds, succs)) =>
       (i, (fold remove_key xs preds, fold remove_key xs succs))));