src/Pure/library.ML
changeset 30570 8fac7efcce0a
parent 30558 2ef9892114fd
child 30572 8fbc355100f2
     1.1 --- a/src/Pure/library.ML	Wed Mar 18 11:57:28 2009 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Mar 18 15:23:52 2009 +0100
     1.3 @@ -1022,7 +1022,7 @@
     1.4  
     1.5  (*insert tags*)
     1.6  fun tag_list k [] = []
     1.7 -  | tag_list k (x :: xs) = (k, x) :: tag_list (k + 1) xs;
     1.8 +  | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs;
     1.9  
    1.10  (*remove tags and suppress duplicates -- list is assumed sorted!*)
    1.11  fun untag_list [] = []