src/Pure/General/table.ML
changeset 29004 a5a91f387791
parent 28334 7c693bb76366
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/table.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/Pure/General/table.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -41,7 +41,6 @@
     1.4    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
     1.5    val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
     1.6    val make: (key * 'a) list -> 'a table                                (*exception DUP*)
     1.7 -  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
     1.8    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     1.9      'a table * 'a table -> 'a table                                    (*exception DUP*)
    1.10    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
    1.11 @@ -364,9 +363,7 @@
    1.12  
    1.13  (* simultaneous modifications *)
    1.14  
    1.15 -fun extend (table, args) = fold update_new args table;
    1.16 -
    1.17 -fun make entries = extend (empty, entries);
    1.18 +fun make entries = fold update_new entries empty;
    1.19  
    1.20  fun join f (table1, table2) =
    1.21    let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;