| changeset 18989 | a5c3bc6fd6b6 |
| parent 18966 | dc49d8b18886 |
| child 19011 | d1c3294ca417 |
--- a/src/Pure/library.ML Fri Feb 10 02:22:16 2006 +0100 +++ b/src/Pure/library.ML Fri Feb 10 02:22:19 2006 +0100 @@ -925,8 +925,9 @@ fun (x: string) mem_string xs = member (op =) xs x; fun x ins xs = insert (op =) x xs; -fun (x:int) ins_int xs = insert (op =) x xs; -fun (x:string) ins_string xs = insert (op =) x xs; +fun (x: int) ins_int xs = insert (op =) x xs; +fun (x: string) ins_string xs = insert (op =) x xs; + (*union of sets represented as lists: no repetitions*) fun xs union [] = xs