equal
deleted
inserted
replaced
117 raised exn ("THM " ^ string_of_int i) |
117 raised exn ("THM " ^ string_of_int i) |
118 (msg :: robust_context context Display.string_of_thm thms) |
118 (msg :: robust_context context Display.string_of_thm thms) |
119 | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); |
119 | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); |
120 in [((i, msg), id)] end) |
120 in [((i, msg), id)] end) |
121 and sorted_msgs context exn = |
121 and sorted_msgs context exn = |
122 sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn)); |
122 sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn)); |
123 |
123 |
124 in sorted_msgs NONE e end; |
124 in sorted_msgs NONE e end; |
125 |
125 |
126 end; |
126 end; |
127 |
127 |