--- 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;