# HG changeset patch
# User wenzelm
# Date 881062688 -3600
# Node ID b75312b2676d5335e058dfe67278deadf3285f96
# Parent  68619c232262e266395f5754b5eaa25660036c20
added context.ML;

diff -r 68619c232262 -r b75312b2676d src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Tue Dec 02 12:37:44 1997 +0100
+++ b/src/Pure/Thy/ROOT.ML	Tue Dec 02 12:38:08 1997 +0100
@@ -1,7 +1,5 @@
 (*  Title:      Pure/Thy/ROOT.ML
     ID:         $Id$
-    Author:     Sonia Mahjoub and Tobias Nipkow and
-                Markus Wenzel and Carsten Clasohm, TU Muenchen
 
 This file builds the theory parser and autoloading system.
 *)
@@ -14,44 +12,11 @@
 use "thy_parse.ML";
 use "thy_syn.ML";
 
+use "context.ML";
+
 use "thy_info.ML";
 use "browser_info.ML";
 use "thm_database.ML";
 use "thy_read.ML";
 
 open ThmDatabase ThyRead ThyInfo BrowserInfo;
-
-
-
-(* FIXME tmp, move *)
-
-structure Session =
-struct
-
-local
-  val current_session = ref ([]: string list);
-in
-  fun get_session () = ! current_session;
-  fun add_session s =
-    (current_session := ! current_session @ [s];
-      writeln ("This is the " ^ quote (space_implode "/" (get_session ())) ^ " session."));
-end;
-
-end;
-
-open Session
-
-
-structure Context =
-struct
-
-local
-  val current_thy = ref ProtoPure.thy;
-in
-  fun context thy = current_thy := thy;
-  fun get_context () = ! current_thy;
-end;
-
-end;
-
-open Context;