--- a/src/Pure/General/graph.ML Sun Aug 28 19:48:15 2005 +0200
+++ b/src/Pure/General/graph.ML Mon Aug 29 08:34:24 2005 +0200
@@ -27,7 +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 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
@@ -144,8 +144,8 @@
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 default_node (x, info) (Graph tab) =
+ Graph (Table.default (x, (info, ([], []))) tab);
fun del_nodes xs (Graph tab) =
Graph (tab
--- a/src/Pure/General/table.ML Sun Aug 28 19:48:15 2005 +0200
+++ b/src/Pure/General/table.ML Mon Aug 29 08:34:24 2005 +0200
@@ -35,7 +35,7 @@
val lookup: 'a table * key -> 'a option
val update: (key * 'a) * 'a table -> 'a table
val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*)
- val default: key -> 'a -> 'a table -> 'a table
+ val default: key * 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUPS*)
val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*)
@@ -204,7 +204,7 @@
fun update ((key, x), tab) = modify key (fn _ => x) tab;
fun update_new ((key, x), tab) = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
-fun default key x tab = if defined tab key then tab else update ((key, x), tab)
+fun default (p as (key, x)) tab = if defined tab key then tab else update (p, tab)
fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);