minor internal changes;

--- a/src/Pure/Syntax/ROOT.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -31,8 +31,5 @@
   and SExtension = SExtension);
 structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
   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;
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 

--- a/src/Pure/Syntax/ast.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/ast.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -7,24 +7,29 @@
 
 signature AST0 =
 sig
-  structure Pretty: PRETTY
   datatype ast =
     Constant of string |
     Variable of string |
     Appl of ast list
+  exception AST of string * ast list
+end;
+
+signature AST1 =
+sig
+  include AST0
+  structure Pretty: PRETTY
   val mk_appl: ast -> ast list -> ast
-  exception AST of string * ast list
   val str_of_ast: ast -> string
   val pretty_ast: ast -> Pretty.T
-  val pretty_rule: (ast * ast) -> Pretty.T
+  val pretty_rule: ast * ast -> Pretty.T
   val pprint_ast: ast -> pprint_args -> unit
   val trace_norm_ast: bool ref
   val stat_norm_ast: bool ref
-end
+end;
 
 signature AST =
 sig
-  include AST0
+  include AST1
   val raise_ast: string -> ast list -> 'a
   val head_of_rule: ast * ast -> string
   val rule_error: ast * ast -> string option

--- a/src/Pure/Syntax/earley0A.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/earley0A.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -412,7 +412,7 @@
 fun unknown c = error ("Unparsable category: " ^ c);
 
 fun syn_err toks =
-  error ("Syntax error at: " ^ space_implode " " (map str_of_token toks));
+  error ("Syntax error at: " ^ quote (space_implode " " (map str_of_token toks)));
 
 fun parse ((_, _, (tab, opLA, rchA)):gram) (root:string) (tl: token list): parsetree =
   let

--- a/src/Pure/Syntax/parser.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -271,7 +271,7 @@
 
 
 fun syntax_error toks =
-  error ("Syntax error at: " ^ space_implode " " (map str_of_token toks));
+  error ("Syntax error at: " ^ quote (space_implode " " (map str_of_token toks)));
 
 fun produce grammar stateset i indata =
   (case Array.sub (stateset, i) of

--- a/src/Pure/Syntax/printer.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/printer.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -32,7 +32,7 @@
 
 functor PrinterFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
   and SExtension: SEXTENSION sharing TypeExt.SynExt = SExtension.Parser.SynExt)
-  (*: PRINTER *) = (* FIXME *)
+  : PRINTER =
 struct
 
 structure Symtab = Symtab;
@@ -213,8 +213,6 @@
 
 (** pretty term or typ asts **)
 
-(*assumes a syntax derived from Pure, otherwise may loop forever*)
-
 fun pretty prtab trf type_mode ast0 p0 =
   let
     val trans = apply_trans "print ast translation";

--- a/src/Pure/Syntax/type_ext.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -6,7 +6,6 @@
 
 TODO:
   term_of_typ: prune sorts
-  move "_K", "_explode", "_implode"
 *)
 
 signature TYPE_EXT0 =
@@ -188,7 +187,7 @@
    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)],
    [],
    [],