equal
deleted
inserted
replaced
70 |
70 |
71 |
71 |
72 (* identification via serial numbers *) |
72 (* identification via serial numbers *) |
73 |
73 |
74 fun identify default_props exn = |
74 fun identify default_props exn = |
75 if Exn.is_interrupt exn then exn |
75 if Exn.is_interrupt_proper exn then exn |
76 else |
76 else |
77 let |
77 let |
78 val props = get exn; |
78 val props = get exn; |
79 val update_serial = |
79 val update_serial = |
80 if Properties.defined props Markup.serialN then [] |
80 if Properties.defined props Markup.serialN then [] |