# HG changeset patch # User paulson # Date 1263315359 0 # Node ID 77f0d11dec7645c24bc30c726b591df4d678df9d # Parent d7786f56f081c5a53fcc497842cd9fc97d6c0c32 Parsing errors during proof reconstruction now give rise to an intelligible error message. diff -r d7786f56f081 -r 77f0d11dec76 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Tue Jan 12 13:36:01 2010 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Jan 12 16:55:59 2010 +0000 @@ -454,7 +454,7 @@ val _ = trace "\ndecode_tstp_file: finishing\n" in isar_header (map #1 fixes) ^ implode ilines ^ "qed\n" - end; + end handle STREE _ => error "Could not extract proof (ATP output malformed?)"; (*=== EXTRACTING PROOF-TEXT === *)