# HG changeset patch
# User wenzelm
# Date 858701035 -3600
# Node ID 174d03b1798f6988e8c3ae7a37fe8a736f5be01e
# Parent  e8a224e41b9f946e161cf0cedf0e743bc708b60e
added dummy set_session;

diff -r e8a224e41b9f -r 174d03b1798f src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Tue Mar 18 17:03:05 1997 +0100
+++ b/src/Pure/Thy/ROOT.ML	Tue Mar 18 17:03:55 1997 +0100
@@ -35,3 +35,9 @@
     "ThmDB.thm_db := !thm_db;",
     "open ThmDB ReadThy;",
     "read_thy_reader_files ();"];
+
+
+(* FIXME tmp *)
+
+fun set_session s =
+  writeln ("This is the " ^ quote s ^ " session.");