diff -r bf45fd2488a2 -r 1403595ec38c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
@@ -610,6 +610,7 @@
                   extract_tstplike_proof_and_outcome verbose complete res_code
                       proof_delims known_failures output
                   |>> atp_proof_from_tstplike_proof atp_problem
+                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
                 val (conjecture_shape, facts_offset, fact_names,
                      typed_helpers) =
                   if is_none outcome then