tuned;

--- a/src/Pure/Syntax/parser.ML	Tue Jan 30 19:45:08 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Jan 30 19:59:15 2018 +0100
@@ -26,6 +26,23 @@
 
 (** datatype gram **)
 
+(* nonterminals *)
+
+(*production for the NTs are stored in a vector
+  so we can identify NTs by their index*)
+type nt = int;
+
+type nts = Inttab.set;
+val nts_empty: nts = Inttab.empty;
+val nts_merge: nts * nts -> nts = Inttab.merge (K true);
+fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
+fun nts_member (nts: nts) = Inttab.defined nts;
+fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
+fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
+fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
+fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
+
+
 (* tokens *)
 
 fun tokens_match toks =
@@ -52,23 +69,8 @@
 val tokens_subtract = tokens_fold tokens_remove;
 fun tokens_find P (tokens: tokens) =
   Tokens.get_first (fn (tok, ()) => if P tok then SOME tok else NONE) tokens;
-
-
-(* nonterminals *)
-
-(*production for the NTs are stored in a vector
-  so we can identify NTs by their index*)
-type nt = int;
+fun tokens_add (nt: nt, tokens) = if tokens_is_empty tokens then I else cons (nt, tokens);
 
-type nts = Inttab.set;
-val nts_empty: nts = Inttab.empty;
-val nts_merge: nts * nts -> nts = Inttab.merge (K true);
-fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
-fun nts_member (nts: nts) = Inttab.defined nts;
-fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
-fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
-fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
-fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
 
 datatype symb =
   Terminal of Lexicon.token
@@ -155,14 +157,14 @@
               val ((_, from_tks), _) = Array.sub (prods, the chain);
 
               (*copy from's lookahead to chain's destinations*)
-              fun copy_lookahead to added =
+              fun copy_lookahead to =
                 let
                   val ((to_nts, to_tks), ps) = Array.sub (prods, to);
 
                   val new_tks = tokens_subtract to_tks from_tks;  (*added lookahead tokens*)
                   val to_tks' = tokens_merge (to_tks, new_tks);
                   val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
-                in if tokens_is_empty new_tks then added else (to, new_tks) :: added end;
+                in tokens_add (to, new_tks) end;
 
               val tos = chains_all_succs chains' [lhs];
             in
@@ -260,9 +262,7 @@
                             is used to access existing
                             productions we have to add new
                             tokens at the _end_ of the list*)
-                        val added_starts' =
-                          if tokens_is_empty added_tks then added_starts
-                          else ((nt, added_tks) :: added_starts);
+                        val added_starts' = tokens_add (nt, added_tks) added_starts;
                       in (added_lambdas', added_starts') end;
 
                     val (added_lambdas, added_starts') =
@@ -344,11 +344,7 @@
                         else
                           Array.update
                             (prods, nt, ((old_nts, tokens_merge (old_tks, new_tks)), nt_prods'));
-                    in
-                      add_tks nts
-                        (if tokens_is_empty new_tks then added else (nt, new_tks) :: added)
-                        prod_count'
-                    end;
+                    in add_tks nts (tokens_add (nt, new_tks) added) prod_count' end;
               val _ = nts_fold add_nts start_nts true;
             in
               add_tks (chains_all_succs chains' [lhs]) [] prod_count
@@ -404,9 +400,9 @@
                           in update_prods ps result end;
 
                     (*copy existing productions for new starting tokens*)
-                    fun process_nts nt added =
+                    fun process_nts nt =
                       let
-                        val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+                        val ((nts, tks), nt_prods) = Array.sub (prods, nt);
 
                         val tk_prods = prods_lookup nt_prods key;
 
@@ -418,16 +414,10 @@
                             prods_update (key, tk_prods') nt_prods'
                           else nt_prods';
 
-                        val added_tks = tokens_subtract old_tks new_tks;
-                      in
-                        if tokens_is_empty added_tks then
-                          (Array.update (prods, nt, (lookahead, nt_prods''));
-                            added)
-                        else
-                          (Array.update
-                             (prods, nt, ((old_nts, tokens_merge (old_tks, added_tks)), nt_prods''));
-                            ((nt, added_tks) :: added))
-                      end;
+                        val added_tks = tokens_subtract tks new_tks;
+                        val tks' = tokens_merge (tks, added_tks);
+                        val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
+                      in tokens_add (nt, added_tks) end;
 
                     val ((dependent, _), _) = Array.sub (prods, changed_nt);
                   in add_starts (starts @ nts_fold process_nts dependent []) end;