src/Pure/General/graph.ML

 signature GRAPH =
 sig
   type key
   type 'a T
   exception DUP of key
-  exception DUPS of key list
   exception SAME
   exception UNDEF of key
   val empty: 'a T
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list

   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*)
+  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
-    'a T * 'a T -> 'a T                                               (*exception DUPS*)
+    'a T * 'a T -> 'a T                                               (*exception DUP*)
   val irreducible_paths: 'a T -> key * key -> key list list
   val all_paths: 'a T -> key * key -> key list list
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)

 (* graphs *)
 
 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
 
 exception DUP = Table.DUP;
-exception DUPS = Table.DUPS;
 exception UNDEF = Table.UNDEF;
 exception SAME = Table.SAME;
 
 val empty = Graph Table.empty;
 fun keys (Graph tab) = Table.keys tab;