diff -r 29d39c10822e -r 427df66052a1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -101,10 +101,10 @@
 
 (* print (ast) translations *)
 
-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);
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+fun extend_tr'tab trfuns = fold_rev Symtab.update_list trfuns;
+fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
+fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
 
 
 
@@ -154,9 +154,9 @@
 
 (* empty, extend, merge ruletabs *)
 
-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);
+val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r));
+val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
+fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
 
 
 
@@ -403,7 +403,7 @@
     val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   in
     SynTrans.asts_to_terms context (lookup_tr parse_trtab)
-      (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
+      (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
   end;
 
 
@@ -487,7 +487,7 @@
   in
     prt_t context curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
-      (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
+      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
   end;
 
 val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;