src/Pure/Syntax/printer.ML

--- a/src/Pure/Syntax/printer.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Syntax/printer.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -188,11 +188,11 @@
 
 (*find tab for mode*)
 fun get_tab prtabs mode =
-  if_none (assoc (prtabs, mode)) Symtab.empty;
+  getOpt (assoc (prtabs, mode), Symtab.empty);
 
 (*collect tabs for mode hierarchy (default "")*)
 fun tabs_of prtabs modes =
-  mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]);
+  List.mapPartial (fn mode => assoc (prtabs, mode)) (modes @ [""]);
 
 
 (* xprod_to_fmt *)
@@ -244,9 +244,9 @@
 
 fun extend_prtabs prtabs mode xprods =
   let
-    val fmts = mapfilter xprod_to_fmt xprods;
+    val fmts = List.mapPartial xprod_to_fmt xprods;
     val tab = get_tab prtabs mode;
-    val new_tab = foldr Symtab.update_multi (rev fmts, tab);
+    val new_tab = Library.foldr Symtab.update_multi (rev fmts, tab);
   in overwrite (prtabs, (mode, new_tab)) end;
 
 fun merge_prtabs prtabs1 prtabs2 =