changeset 3879 | de18c0c1141c |
parent 3873 | 64f496e0885d |
child 3936 | 1954255c29ef |
--- a/src/Pure/display.ML Wed Oct 15 15:18:41 1997 +0200 +++ b/src/Pure/display.ML Thu Oct 16 10:22:37 1997 +0200 @@ -150,8 +150,8 @@ fun less_idx ((x, i):indexname, (y, j):indexname) = x < y orelse x = y andalso i < j; - val sort_idxs = map (apsnd (sort less_idx)); - val sort_strs = map (apsnd sort_strings); + fun sort_idxs l = map (apsnd (sort less_idx)) l; + fun sort_strs l = map (apsnd sort_strings) l; (* prepare atoms *)