# HG changeset patch
# User wenzelm
# Date 777303383 -7200
# Node ID fc92fac8b0deef6333ac56e40e94643b2c58533e
# Parent  4c139c37dbafff4a4fc96593afb3577a3d42ddf1
removed roots arg of extend_gram;
added functor sig constraint (: PARSER);

diff -r 4c139c37dbaf -r fc92fac8b0de src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Aug 19 15:35:56 1994 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Aug 19 15:36:23 1994 +0200
@@ -2,10 +2,7 @@
     ID:         $Id$
     Author:     Sonia Mahjoub, Markus Wenzel and Carsten Clasohm, TU Muenchen
 
-Isabelle's main parser (used for terms and typs).
-
-TODO:
-  extend_gram: remove 'roots' arg
+Isabelle's main parser (used for terms and types).
 *)
 
 signature PARSER =
@@ -15,7 +12,7 @@
   local open Lexicon SynExt SynExt.Ast in
     type gram
     val empty_gram: gram
-    val extend_gram: gram -> string list -> xprod list -> gram
+    val extend_gram: gram -> xprod list -> gram
     val merge_grams: gram -> gram -> gram
     val pretty_gram: gram -> Pretty.T list
     datatype parsetree =
@@ -26,7 +23,7 @@
 end;
 
 functor ParserFun(structure Symtab: SYMTAB and Lexicon: LEXICON
-  and SynExt: SYN_EXT) =
+  and SynExt: SYN_EXT): PARSER =
 struct
 
 structure Pretty = SynExt.Ast.Pretty;
@@ -260,7 +257,7 @@
 
 val empty_gram = mk_gram [];
 
-fun extend_gram (gram1 as Gram (prods1, _)) _ xprods2 =
+fun extend_gram (gram1 as Gram (prods1, _)) xprods2 =
   let
     fun symb_of (Delim s) = Some (Terminal (Token s))
       | symb_of (Argument (s, p)) =