diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -191,8 +191,8 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-fun mode_tab prtabs mode = if_none (assoc (prtabs, mode)) Symtab.empty;
-fun mode_tabs prtabs modes = List.mapPartial (curry assoc prtabs) (modes @ [""]);
+fun mode_tab prtabs mode = if_none (AList.lookup (op =) prtabs mode) Symtab.empty;
+fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
 
 
 (* xprod_to_fmt *)