changeset 15759 | 144c9f9a8ade |
parent 15753 | eb014dfc57ee |
child 15834 | a5166d054683 |
--- a/src/Pure/Syntax/printer.ML Sun Apr 17 19:38:53 2005 +0200 +++ b/src/Pure/Syntax/printer.ML Sun Apr 17 19:39:11 2005 +0200 @@ -250,7 +250,7 @@ in overwrite (prtabs, (mode, tab)) end; fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m; -fun remove_prtabs m = change_prtabs (fn (c, prnp) => Symtab.map_entry c (remove prnp)) m; +fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m; fun merge_prtabs prtabs1 prtabs2 = let