--- a/src/Pure/General/table.ML Wed Aug 24 12:07:00 2005 +0200
+++ b/src/Pure/General/table.ML Thu Aug 25 09:23:13 2005 +0200
@@ -35,6 +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 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*)
@@ -203,6 +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 map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);