equal
deleted
inserted
replaced
338 Branch2 (mr, if_eq ord q' q, r')))))); |
338 Branch2 (mr, if_eq ord q' q, r')))))); |
339 |
339 |
340 in |
340 in |
341 |
341 |
342 fun delete key tab = snd (snd (del (SOME key) tab)); |
342 fun delete key tab = snd (snd (del (SOME key) tab)); |
343 fun delete_safe key tab = delete key tab handle UNDEF _ => tab; |
343 fun delete_safe key tab = if defined tab key then delete key tab else tab; |
344 |
344 |
345 end; |
345 end; |
346 |
346 |
347 |
347 |
348 (* membership operations *) |
348 (* membership operations *) |