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