src/Pure/Thy/present.ML
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 *)