diff -r 192c48376d25 -r f600215b6ea7 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/parser.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -6,33 +6,24 @@
 *)
 
 signature PARSER =
-sig
-  structure Lexicon: LEXICON
-  structure SynExt: SYN_EXT
-  local open Lexicon SynExt SynExt.Ast in
-    type gram
-    val empty_gram: gram
-    val extend_gram: gram -> xprod list -> gram
-    val merge_grams: gram -> gram -> gram
-    val pretty_gram: gram -> Pretty.T list
-    datatype parsetree =
-      Node of string * parsetree list |
-      Tip of token
-    val parse: gram -> string -> token list -> parsetree list
-  end
-  val branching_level: int ref;
-end;
+  sig
+  type gram
+  val empty_gram: gram
+  val extend_gram: gram -> SynExt.xprod list -> gram
+  val merge_grams: gram -> gram -> gram
+  val pretty_gram: gram -> Pretty.T list
+  datatype parsetree =
+    Node of string * parsetree list |
+    Tip of Lexicon.token
+  val parse: gram -> string -> Lexicon.token list -> parsetree list
+  val branching_level: int ref
+  end;
 
-functor ParserFun(structure Symtab: SYMTAB and Lexicon: LEXICON
-  and SynExt: SYN_EXT): PARSER =
+
+structure Parser : PARSER =
 struct
-
-structure Pretty = SynExt.Ast.Pretty;
-structure Lexicon = Lexicon;
-structure SynExt = SynExt;
 open Lexicon SynExt;
 
-
 (** datatype gram **)
 
 type nt_tag = int;              (*production for the NTs are stored in an array