# 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 === *)