Parsing errors during proof reconstruction now give rise to an intelligible error message.

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