equal
deleted
inserted
replaced
190 else |
190 else |
191 (really_go () |
191 (really_go () |
192 handle |
192 handle |
193 ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") |
193 ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") |
194 | exn => |
194 | exn => |
195 if Exn.is_interrupt exn then reraise exn |
195 if Exn.is_interrupt exn then Exn.reraise exn |
196 else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) |
196 else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) |
197 |
197 |
198 val _ = |
198 val _ = |
199 (* The "expect" argument is deliberately ignored if the prover is |
199 (* The "expect" argument is deliberately ignored if the prover is |
200 missing so that the "Metis_Examples" can be processed on any |
200 missing so that the "Metis_Examples" can be processed on any |