# HG changeset patch
# User wenzelm
# Date 1302008695 -7200
# Node ID cb650789f2f0f6bcc98d43ecd37b74e63cc9c2c9
# Parent  cf48af3062900ca3ee7abd43390c43ed7f4291e7
use standard tables with standard argument order;

diff -r cf48af306290 -r cb650789f2f0 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Apr 05 14:30:40 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Apr 05 15:04:55 2011 +0200
@@ -671,22 +671,15 @@
         in (n, (t', prec') :: ts') end;
 
 (*Update entry in used*)
-fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) =
-  if A = B then
-    let val (n, ts') = conc t ts
-    in ((A, (i, ts')) :: used, n) end
-  else
-    let val (used', n) = update_trees used (A, t)
-    in ((B, (i, ts)) :: used', n) end;
+fun update_trees (A, t) used =
+  let
+    val (i, ts) = the (Inttab.lookup used A);
+    val (n, ts') = conc t ts;
+  in (n, Inttab.update (A, (i, ts')) used) end;
 
 (*Replace entry in used*)
-fun update_prec (A: nt_tag, prec) used =
-  let
-    fun update ((hd as (B, (_, ts))) :: used, used') =
-      if A = B
-      then used' @ ((A, (prec, ts)) :: used)
-      else update (used, hd :: used')
-  in update (used, []) end;
+fun update_prec (A, prec) =
+  Inttab.map_entry A (fn (_, ts) => (prec, ts));
 
 fun getS A max_prec NONE Si =
       filter
@@ -752,7 +745,7 @@
             (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) =>
               let (*predictor operation*)
                 val (used', new_states) =
-                  (case AList.lookup (op =) used nt of
+                  (case Inttab.lookup used nt of
                     SOME (used_prec, l) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
@@ -767,7 +760,7 @@
                       let
                         val tk_prods = all_prods_for nt;
                         val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
-                      in ((nt, (min_prec, [])) :: used, States') end);
+                      in (Inttab.update (nt, (min_prec, [])) used, States') end);
 
                 val _ =
                   if not (! warned) andalso
@@ -787,7 +780,7 @@
               let val tt = if id = "" then ts else [Node (id, rev ts)] in
                 if j = i then (*lambda production?*)
                   let
-                    val (used', prec') = update_trees used (A, (tt, prec));
+                    val (prec', used') = update_trees (A, (tt, prec)) used;
                     val Slist = getS A prec prec' Si;
                     val States' = map (movedot_nonterm tt) Slist;
                   in processS used' (States' @ States) (S :: Si, Sii) end
@@ -795,7 +788,7 @@
                   let val Slist = get_states Estate i j A prec
                   in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
               end)
-  in processS [] states ([], []) end;
+  in processS Inttab.empty states ([], []) end;
 
 
 fun produce ctxt warned prods tags chains stateset i indata prev_token =