--- a/src/Pure/Syntax/parser.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 15 17:16:56 2005 +0200
@@ -446,9 +446,9 @@
let
(*Get tag for existing nonterminal or create a new one*)
fun get_tag nt_count tags nt =
- case Symtab.curried_lookup tags nt of
+ case Symtab.lookup tags nt of
SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
+ | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
nt_count);
(*Convert symbols to the form used by the parser;
@@ -523,9 +523,9 @@
(*get existing tag from grammar1 or create a new one*)
fun get_tag nt_count tags nt =
- case Symtab.curried_lookup tags nt of
+ case Symtab.lookup tags nt of
SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
+ | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
nt_count)
val ((nt_count1', tags1'), tag_table) =
@@ -868,7 +868,7 @@
fun earley prods tags chains startsymbol indata =
let
- val start_tag = case Symtab.curried_lookup tags startsymbol of
+ val start_tag = case Symtab.lookup tags startsymbol of
SOME tag => tag
| NONE => error ("parse: Unknown startsymbol " ^
quote startsymbol);