# HG changeset patch
# User wenzelm
# Date 1313872133 -7200
# Node ID 59ff5a93eef489c402c155dc88d36852928ac754
# Parent  156be0e433361d29a55cae58880f59de46a37716
tuned Table.delete_safe: avoid potentially expensive attempt of delete;

diff -r 156be0e43336 -r 59ff5a93eef4 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Aug 20 20:24:12 2011 +0200
+++ b/src/Pure/General/table.ML	Sat Aug 20 22:28:53 2011 +0200
@@ -340,7 +340,7 @@
 in
 
 fun delete key tab = snd (snd (del (SOME key) tab));
-fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
+fun delete_safe key tab = if defined tab key then delete key tab else tab;
 
 end;