src/Pure/Syntax/printer.ML
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