| changeset 59058 | a78612c67ec0 |
| parent 58870 | e2c0d8ef29cb |
| child 59173 | cdcbda56b05b |
--- a/src/Pure/Thy/present.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Thy/present.ML Wed Nov 26 20:05:34 2014 +0100 @@ -277,7 +277,7 @@ (* finish session -- output all generated text *) -fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index)); +fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; fun write_tex src name path =