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