src/Pure/Syntax/parser.ML

   | extend_gram (Gram {nt_count, prod_count, tags, chains, lambdas, prods})
                 xprods =
   let
     (*Get tag for existing nonterminal or create a new one*)
     fun get_tag nt_count tags nt =
-      case Symtab.lookup (tags, nt) of
+      case Symtab.curried_lookup tags nt of
         SOME tag => (nt_count, tags, tag)
-      | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
+      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
                  nt_count);
 
     (*Convert symbols to the form used by the parser;
       delimiters and predefined terms are stored as terminals,
       nonterminals are converted to integer tags*)

                               else (gram_b, gram_a)
       end;
 
     (*get existing tag from grammar1 or create a new one*)
     fun get_tag nt_count tags nt =
-      case Symtab.lookup (tags, nt) of
+      case Symtab.curried_lookup tags nt of
         SOME tag => (nt_count, tags, tag)
-      | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
+      | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
                 nt_count)
 
     val ((nt_count1', tags1'), tag_table) =
       let val tag_list = Symtab.dest tags2;
 

 fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
                             l;
 
 fun earley prods tags chains startsymbol indata =
   let
-    val start_tag = case Symtab.lookup (tags, startsymbol) of
+    val start_tag = case Symtab.curried_lookup tags startsymbol of
                        SOME tag => tag
                      | NONE   => error ("parse: Unknown startsymbol " ^
                                         quote startsymbol);
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal EndToken],
                "", 0)];