# HG changeset patch
# User wenzelm
# Date 1139776463 -3600
# Node ID 8635700e2c9cbfb0e06ecf986467c6f8bec4f6a5
# Parent  6c238953f66c4c234edc83f92473e19fa6e68930
share exception UNDEF with Table;
simplified TableFun.join;

diff -r 6c238953f66c -r 8635700e2c9c src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sun Feb 12 21:34:22 2006 +0100
+++ b/src/Pure/General/graph.ML	Sun Feb 12 21:34:23 2006 +0100
@@ -9,9 +9,10 @@
 sig
   type key
   type 'a T
-  exception UNDEF of key
   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
@@ -37,7 +38,8 @@
   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 join: (key -> 'a * 'a -> 'a option) -> 'a T * 'a T -> 'a T      (*exception DUPS*)
+  val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
+    'a T * 'a T -> 'a T                                               (*exception DUPS*)
   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*)
@@ -74,9 +76,10 @@
 
 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
 
-exception UNDEF of key;
 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;
@@ -205,9 +208,7 @@
 fun no_edges (i, _) = (i, ([], []));
 
 fun join f (Graph tab1, G2 as Graph tab2) =
-  let
-    fun join_node key ((i1, edges1), (i2, _)) =
-      (Option.map (rpair edges1) o f key) (i1, i2);
+  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
   in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
 
 fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =