equal
deleted
inserted
replaced
38 |
38 |
39 (* capture exception trace *) |
39 (* capture exception trace *) |
40 |
40 |
41 local |
41 local |
42 fun eq_exn exns = |
42 fun eq_exn exns = |
43 op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Output.position exns); |
43 op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Properties.position exns); |
44 in |
44 in |
45 |
45 |
46 fun capture_exception_trace e = |
46 fun capture_exception_trace e = |
47 uninterruptible (fn restore_attributes => fn () => |
47 uninterruptible (fn restore_attributes => fn () => |
48 let |
48 let |