1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -125,10 +125,10 @@
     1.4  
     1.5  fun get_lexicons () = ! global_lexicons;
     1.6  fun get_parsers () = ! global_parsers;
     1.7 -fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ());
     1.8 +fun get_parser () = Option.map (#2 o #1) o Symtab.lookup (get_parsers ());
     1.9  
    1.10  fun command_tags name =
    1.11 -  (case Symtab.curried_lookup (get_parsers ()) name of
    1.12 +  (case Symtab.lookup (get_parsers ()) name of
    1.13      SOME (((_, k), _), _) => OuterKeyword.tags_of k
    1.14    | NONE => []);
    1.15  
    1.16 @@ -143,7 +143,7 @@
    1.17  fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
    1.18   (if not (Symtab.defined tab name) then ()
    1.19    else warning ("Redefined outer syntax command " ^ quote name);
    1.20 -  Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab);
    1.21 +  Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab);
    1.22  
    1.23  fun add_parsers parsers =
    1.24    (change_parsers (fold add_parser parsers);