tuned Table.delete_safe: avoid potentially expensive attempt of delete;

--- 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;