--- 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;