src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Sep 15 17:16:56 2005 +0200
@@ -82,7 +82,7 @@
 
 (* parse (ast) translations *)
 
-fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c);
+fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
 
 fun err_dup_trfuns name cs =
   error ("More than one " ^ name ^ " for " ^ commas_quote cs);
@@ -98,8 +98,8 @@
 
 (* print (ast) translations *)
 
-fun lookup_tr' tab c = map fst (Symtab.curried_lookup_multi tab c);
-fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns;
+fun lookup_tr' tab c = map fst (Symtab.lookup_multi tab c);
+fun extend_tr'tab trfuns = fold_rev Symtab.update_multi trfuns;
 fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
 fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
 
@@ -151,7 +151,7 @@
 
 (* empty, extend, merge ruletabs *)
 
-val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r));
+val extend_ruletab = fold_rev (fn r => Symtab.update_multi (Ast.head_of_rule r, r));
 val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
 fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
 
@@ -385,7 +385,7 @@
     val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   in
     SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
-      (map (Ast.normalize_ast (Symtab.curried_lookup_multi parse_ruletab)) asts)
+      (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
   end;
 
 
@@ -469,7 +469,7 @@
   in
     prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
-      (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast)
+      (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
   end;
 
 val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;