changeset 18928 | 042608ffa2ec |
parent 18683 | a8f9c192f6d1 |
child 18964 | 67f572e03236 |
--- 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;