| changeset 28375 | c879d88d038a |
| parent 28027 | 051d5ccbafc5 |
| child 28496 | 4cff10648928 |
--- a/src/Pure/Thy/present.ML Fri Sep 26 17:24:15 2008 +0200 +++ b/src/Pure/Thy/present.ML Fri Sep 26 19:07:56 2008 +0200 @@ -273,7 +273,7 @@ fun read_versions strs = rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs))) - |> filter_out (equal "-" o #2); + |> filter_out (fn (_, s) => s = "-"); (* init session *)