| changeset 19482 | 9f11af8f7ef9 |
| parent 19073 | fce515f7759c |
| child 19506 | 980a2edf9e82 |
--- a/src/Pure/General/table.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/table.ML Thu Apr 27 15:06:35 2006 +0200 @@ -379,7 +379,7 @@ handle UNDEF _ => delete key tab; fun make_list args = fold_rev update_list args empty; -fun dest_list tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab)); +fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); fun merge_list eq = join (fn _ => Library.merge eq);