src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Sep 01 18:48:50 2005 +0200
@@ -125,10 +125,10 @@
 
 fun get_lexicons () = ! global_lexicons;
 fun get_parsers () = ! global_parsers;
-fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ());
+fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ());
 
 fun command_tags name =
-  (case Symtab.lookup (get_parsers (), name) of
+  (case Symtab.curried_lookup (get_parsers ()) name of
     SOME (((_, k), _), _) => OuterKeyword.tags_of k
   | NONE => []);
 
@@ -143,7 +143,7 @@
 fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
  (if not (Symtab.defined tab name) then ()
   else warning ("Redefined outer syntax command " ^ quote name);
-  Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
+  Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab);
 
 fun add_parsers parsers =
   (change_parsers (fold add_parser parsers);