tuned Table.delete_safe: avoid potentially expensive attempt of delete;
authorwenzelm
Sat Aug 20 22:28:53 2011 +0200 (2011-08-20)
changeset 4433659ff5a93eef4
parent 44335 156be0e43336
child 44337 d453faed4815
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
src/Pure/General/table.ML
     1.1 --- a/src/Pure/General/table.ML	Sat Aug 20 20:24:12 2011 +0200
     1.2 +++ b/src/Pure/General/table.ML	Sat Aug 20 22:28:53 2011 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4  in
     1.5  
     1.6  fun delete key tab = snd (snd (del (SOME key) tab));
     1.7 -fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
     1.8 +fun delete_safe key tab = if defined tab key then delete key tab else tab;
     1.9  
    1.10  end;
    1.11