minor internal changes;

--- a/src/Pure/Syntax/ROOT.ML	Wed Jan 19 14:22:37 1994 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Wed Jan 19 14:23:18 1994 +0100
@@ -6,12 +6,9 @@
 *)
 
 use "pretty.ML";
-
+use "lexicon.ML";
 use "ast.ML";
-use "xgram.ML";
-use "lexicon.ML";
-use "extension.ML";
-use "parse_tree.ML";
+use "syn_ext.ML";
 use "parser.ML";
 use "earley0A.ML";
 use "type_ext.ML";
@@ -20,26 +17,20 @@
 use "syntax.ML";
 
 structure Pretty = PrettyFun();
-
+structure Lexicon = LexiconFun();
+structure Scanner: SCANNER = Lexicon;
 structure Ast = AstFun(Pretty);
-structure XGram = XGramFun(Ast);
-structure Lexicon = LexiconFun();
-structure Extension = ExtensionFun(structure XGram = XGram and Lexicon = Lexicon);
-structure ParseTree = ParseTreeFun(structure Ast = Ast and Lexicon = Lexicon);
-structure Parser = ParserFun(structure Symtab = Symtab and XGram = XGram
-  and ParseTree = ParseTree);
-structure Earley = EarleyFun(structure Symtab = Symtab and XGram = XGram
-  and ParseTree = ParseTree);
-structure TypeExt = TypeExtFun(structure Extension = Extension
-  and Lexicon = Lexicon);
-structure SExtension = SExtensionFun(structure TypeExt = TypeExt
-  and Lexicon = Lexicon);
-structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
-  and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
+structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast);
+structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
+  and SynExt = SynExt);
+structure Earley = EarleyFun(structure Symtab = Symtab and Lexicon = Lexicon
+  and SynExt = SynExt);
+structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
+structure SExtension = SExtensionFun(Earley);
+structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt
+  and SExtension = SExtension);
 structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
-  and Parser = Earley and SExtension = SExtension and Printer = Printer);
-
-structure Scanner: SCANNER = Lexicon;
+  and SExtension = SExtension and Printer = Printer);
 
 (*BasicSyntax has the most important primitives, which are made pervasive*)
 signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;

--- a/src/Pure/Syntax/type_ext.ML	Wed Jan 19 14:22:37 1994 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Jan 19 14:23:18 1994 +0100
@@ -6,7 +6,7 @@
 
 TODO:
   term_of_typ: prune sorts
-  move "_K" (?)
+  move "_K", "_explode", "_implode"
 *)
 
 signature TYPE_EXT0 =
@@ -17,19 +17,19 @@
 signature TYPE_EXT =
 sig
   include TYPE_EXT0
-  structure Extension: EXTENSION
-  local open Extension Extension.XGram.Ast in
+  structure SynExt: SYN_EXT
+  local open SynExt SynExt.Ast in
     val term_of_typ: bool -> typ -> term
     val tappl_ast_tr': ast * ast list -> ast
-    val type_ext: ext
+    val type_ext: syn_ext
   end
 end;
 
-functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT =
+functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT =
 struct
 
-structure Extension = Extension;
-open Extension Extension.XGram Extension.XGram.Ast Lexicon;
+structure SynExt = SynExt;
+open Lexicon SynExt SynExt.Ast;
 
 
 (** typ_of_term **)
@@ -170,32 +170,30 @@
 val classesT = Type ("classes", []);
 val typesT = Type ("types", []);
 
-val type_ext =
-  Ext {
-    roots = [logic, "type"],
-    mfix = [
-      Mfix ("_",           tfreeT --> typeT,              "", [], max_pri),
-      Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
-      Mfix ("_",           idT --> typeT,                 "", [], max_pri),
-      Mfix ("_::_",        [tfreeT, sortT] ---> typeT,    "_ofsort", [max_pri, 0], max_pri),
-      Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
-      Mfix ("_",           idT --> sortT,                 "", [], max_pri),
-      Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
-      Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
-      Mfix ("_",           idT --> classesT,              "", [], max_pri),
-      Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
-      Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),  (* FIXME ambiguous *)
-      Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT,      "_tappl", [], max_pri),           (* FIXME ambiguous *)
-      Mfix ("_",           typeT --> typesT,              "", [], max_pri),
-      Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
-      Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
-      Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)],
-    extra_consts = ["_K"],
-    parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr),
-      ("_bracket", bracket_ast_tr)],
-    parse_translation = [],
-    print_translation = [],
-    print_ast_translation = [("fun", fun_ast_tr')]};
+val type_ext = syn_ext
+  [logic, "type"]
+  [Mfix ("_",           tfreeT --> typeT,              "", [], max_pri),
+   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
+   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
+   Mfix ("_::_",        [tfreeT, sortT] ---> typeT,    "_ofsort", [max_pri, 0], max_pri),
+   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
+   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
+   Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
+   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
+   Mfix ("_",           idT --> classesT,              "", [], max_pri),
+   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
+   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),  (* FIXME ambiguous *)
+   Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT,      "_tappl", [], max_pri),           (* FIXME ambiguous *)
+   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
+   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
+   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
+   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
+  ["_K", "_explode", "_implode"]
+  ([("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
+   [],
+   [],
+   [("fun", fun_ast_tr')])
+  ([], []);
 
 
 end;