diff -r 2e5b0f3f1418 -r 042608ffa2ec src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Isar/session.ML	Mon Feb 06 11:01:28 2006 +0100
@@ -41,7 +41,7 @@
 
 fun add_path reset s =
   let val sess = ! session @ [s] in
-    (case Library.duplicates sess of
+    (case gen_duplicates (op =) sess of
       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
     | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
   end;