1.1 --- a/src/Pure/Thy/present.ML Tue Mar 21 12:18:13 2006 +0100
1.2 +++ b/src/Pure/Thy/present.ML Tue Mar 21 12:18:15 2006 +0100
1.3 @@ -261,7 +261,7 @@
1.4 fun update_index dir name =
1.5 (case try get_entries dir of
1.6 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
1.7 - | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
1.8 + | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
1.9
1.10
1.11 (* document versions *)