changeset 18964 | 67f572e03236 |
parent 18928 | 042608ffa2ec |
child 20664 | ffbc5a57191a |
--- a/src/Pure/Isar/session.ML Tue Feb 07 08:47:43 2006 +0100 +++ b/src/Pure/Isar/session.ML Tue Feb 07 19:56:45 2006 +0100 @@ -41,7 +41,7 @@ fun add_path reset s = let val sess = ! session @ [s] in - (case gen_duplicates (op =) sess of + (case 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;