diff -r a0dc597d9173 -r 5651e0636e38 src/Pure/Isar/session.ML --- a/src/Pure/Isar/session.ML Thu Jan 18 20:40:33 2001 +0100 +++ b/src/Pure/Isar/session.ML Thu Jan 18 20:40:47 2001 +0100 @@ -32,7 +32,7 @@ fun path () = ! session_path; -fun str_of [] = "Pure" +fun str_of [] = pure | str_of elems = space_implode "/" elems; fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";