src/Pure/Thy/present.ML
changeset 19305 5c16895d548b
parent 19046 bc5c6c9b114e
child 20577 a96883a6d709
     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 *)