changeset 44336 | 59ff5a93eef4 |
parent 43792 | d5803c3d537a |
child 47980 | c81801f881b3 |
--- 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;