# HG changeset patch
# User wenzelm
# Date 954418720 -7200
# Node ID 80992b8566e5afd1890a7dbdd1f71d15ab6858d5
# Parent  625fbbe5c6b4b0c6d12aaf4f83005d0adc51baf3
export update_multi;

diff -r 625fbbe5c6b4 -r 80992b8566e5 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Mar 30 14:15:41 2000 +0200
+++ b/src/Pure/General/table.ML	Thu Mar 30 14:18:40 2000 +0200
@@ -33,6 +33,7 @@
   val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
   val lookup_multi: 'a list table * key -> 'a list
+  val update_multi: (key * 'a) * 'a list table -> 'a list table
   val make_multi: (key * 'a) list -> 'a list table
   val dest_multi: 'a list table -> (key * 'a) list
 end;
@@ -180,10 +181,10 @@
 
 fun lookup_multi tab_key = if_none (lookup tab_key) [];
 
-fun cons_entry ((key, x), tab) =
+fun update_multi ((key, x), tab) =
   update ((key, x :: lookup_multi (tab, key)), tab);
 
-fun make_multi pairs = foldr cons_entry (pairs, empty);
+fun make_multi pairs = foldr update_multi (pairs, empty);
 
 fun dest_multi tab =
   flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));