tuned;

--- a/src/Pure/Syntax/parser.ML	Sat Jan 27 16:56:03 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Jan 27 17:23:21 2018 +0100
@@ -622,7 +622,7 @@
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
-fun prods_for prods chains include_none tk nts =
+fun prods_for (Gram {prods, chains, ...}) include_none tk nts =
   let
     fun token_assoc (list, key) =
       let
@@ -641,9 +641,9 @@
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS prods chains Estate i c states =
+fun PROCESSS gram Estate i c states =
   let
-    fun all_prods_for nt = prods_for prods chains true c [nt];
+    fun all_prods_for nt = prods_for gram true c [nt];
 
     fun processS _ [] (Si, Sii) = (Si, Sii)
       | processS used (S :: States) (Si, Sii) =
@@ -689,7 +689,7 @@
   in processS Inttab.empty states ([], []) end;
 
 
-fun produce prods tags chains stateset i indata prev_token =
+fun produce gram stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
@@ -714,15 +714,15 @@
         [] => s
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS prods chains stateset i c s;
+            val (si, sii) = PROCESSS gram stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
-          in produce prods tags chains stateset (i + 1) cs c end));
+          in produce gram stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
 
-fun earley prods tags chains startsymbol indata =
+fun earley (gram as Gram {tags, ...}) startsymbol indata =
   let
     val start_tag =
       (case Symtab.lookup tags startsymbol of
@@ -733,18 +733,18 @@
     val Estate = Array.array (s, []);
     val _ = Array.update (Estate, 0, S0);
   in
-    get_trees (produce prods tags chains Estate 0 indata Lexicon.eof)
+    get_trees (produce gram Estate 0 indata Lexicon.eof)
   end;
 
 
-fun parse (Gram {tags, prods, chains, ...}) start toks =
+fun parse gram start toks =
   let
     val end_pos =
       (case try List.last toks of
         NONE => Position.none
       | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     val r =
-      (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
+      (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of
         [] => raise Fail "Inner syntax: no parse trees"
       | pts => pts);
   in r end;