diff -r 000000000000 -r a5a9c433f639 src/Pure/Thy/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/ROOT.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Pure/Thy/ROOT
+    ID:         $Id$
+    Author:     Sonia Mahjoub / Tobias Nipkow
+    Copyright   1992  TU Muenchen
+
+This file builds the theory parser.
+It assumes the standard Isabelle environment.
+*)
+
+use "scan.ML";
+use "parse.ML";
+use "syntax.ML";
+use "read.ML";
+
+
+structure Keyword =
+    struct
+    val alphas =  ["classes", "default", "arities", "types",
+                   "consts", "rules", "end", "rules", "mixfix",
+                   "infixr", "infixl", "binder", "translations"]
+
+    val symbols = [",", "<", "{", "}", "(", ")", "(*", "*)",
+                   "[", "]", "::", "=", "+", "==", "=>", "<="]
+    end;
+
+structure Lex     = LexicalFUN (Keyword);
+structure Parse   = ParseFUN (Lex);
+structure ThySyn  = ThySynFUN (Parse);
+structure Readthy = ReadthyFUN (ThySyn);
+
+open Readthy;