src/Pure/symtab.ML
changeset 2672 85d7e800d754
parent 2228 f381c1a98209
child 4483 caf8ae95c61f
     1.1 --- a/src/Pure/symtab.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/symtab.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4    balance (foldr cons_entry (alst, Tip));
     1.5  
     1.6  fun dest_multi tab =
     1.7 -  flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
     1.8 +  List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
     1.9  
    1.10  
    1.11  (* map tables *)