# HG changeset patch
# User wenzelm
# Date 1194786012 -3600
# Node ID 0856e0141062dc2f721f9507f825717915a51578
# Parent  bb8d225dcf05e874c644ec7054b84ce349c51809
replaced extend_prtabs by update_prtabs (absorb duplicates);

diff -r bb8d225dcf05 -r 0856e0141062 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Nov 11 14:00:11 2007 +0100
+++ b/src/Pure/Syntax/printer.ML	Sun Nov 11 14:00:12 2007 +0100
@@ -26,7 +26,7 @@
     (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
-  val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
+  val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
@@ -239,10 +239,10 @@
 
 val empty_prtabs = [];
 
-fun extend_prtabs mode xprods prtabs =
+fun update_prtabs mode xprods prtabs =
   let
     val fmts = map_filter xprod_to_fmt xprods;
-    val tab' = fold Symtab.update_list fmts (mode_tab prtabs mode);
+    val tab' = fold (Symtab.update_list (op =)) fmts (mode_tab prtabs mode);
   in AList.update (op =) (mode, tab') prtabs end;
 
 fun remove_prtabs mode xprods prtabs =
@@ -251,10 +251,8 @@
     val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
       if null (Symtab.lookup_list tab c) then NONE
       else xprod_to_fmt xprod) xprods;
-  in
-    if null fmts then prtabs
-    else AList.update (op =) (mode, fold (Symtab.remove_list (op =)) fmts tab) prtabs
-  end;
+    val tab' = fold (Symtab.remove_list (op =)) fmts tab;
+  in AList.update (op =) (mode, tab') prtabs end;
 
 fun merge_prtabs prtabs1 prtabs2 =
   let