src/Pure/General/graph.ML

   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
   val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
 end;
 
-functor GraphFun(Key: KEY): GRAPH =
+functor Graph(Key: KEY): GRAPH =
 struct
 
 (* keys *)
 
 type key = Key.key;

 val remove_key = remove eq_key;
 
 
 (* tables and sets of keys *)
 
-structure Table = TableFun(Key);
+structure Table = Table(Key);
 type keys = unit Table.table;
 
 val empty_keys = Table.empty: keys;
 
 fun member_keys tab = Table.defined (tab: keys);

 (*final declarations of this structure!*)
 val fold = fold_graph;
 
 end;
 
-structure Graph = GraphFun(type key = string val ord = fast_string_ord);
-structure IntGraph = GraphFun(type key = int val ord = int_ord);
+structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure IntGraph = Graph(type key = int val ord = int_ord);