# HG changeset patch
# User wenzelm
# Date 921068266 -3600
# Node ID 3b0b5890e1f12704e6765a0b0610779267629c09
# Parent  7d5cbd5819a09aa38ae51ad3653b40c523e1d29c
report path instead of actual session;

diff -r 7d5cbd5819a0 -r 3b0b5890e1f1 src/Pure/Thy/session.ML
--- a/src/Pure/Thy/session.ML	Wed Mar 10 10:55:12 1999 +0100
+++ b/src/Pure/Thy/session.ML	Wed Mar 10 13:17:46 1999 +0100
@@ -32,10 +32,10 @@
 
 (* diagnostics *)
 
-fun str_of [id] = id
-  | str_of ids = space_implode "/" (tl ids);
+fun str_of [] = "Pure"
+  | str_of elems = space_implode "/" elems;
 
-fun welcome () = "Welcome to Isabelle/" ^ str_of (! session) ^ " (" ^ version ^ ")";
+fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
 
 
 (* init *)
@@ -59,12 +59,10 @@
 val root_file = ThyLoad.ml_path "ROOT";
 
 fun use_dir reset info parent name =
-  let val parent_session = ! session in
-    init reset parent name;
-    Present.init info parent_session (! session) (path ()) name;
+  (init reset parent name;
+    Present.init info (path ()) name;
     Symbol.use root_file;
-    finish ()
-  end handle _ => exit 1;
+    finish ()) handle _ => exit 1;
 
 
 end;