changeset 19305 | 5c16895d548b |
parent 19046 | bc5c6c9b114e |
child 20577 | a96883a6d709 |
--- a/src/Pure/Thy/present.ML Tue Mar 21 12:18:13 2006 +0100 +++ b/src/Pure/Thy/present.ML Tue Mar 21 12:18:15 2006 +0100 @@ -261,7 +261,7 @@ fun update_index dir name = (case try get_entries dir of NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) - | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); + | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); (* document versions *)