Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 51878 f11039b31bae
parent 51192 4dc6bb65c3c3
child 52031 9a9238342963 
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 06 11:03:08 2013 +0200
@@ -177,7 +177,9 @@
     fun do_term extra_ts opt_T u =
       case u of
         ATerm ((s, _), us) =>
-        if String.isPrefix native_type_prefix s then
+        if s = ""
+          then error "Isar proof reconstruction failed because the ATP proof contained unparsable material."
+        else if String.isPrefix native_type_prefix s then
           @{const True} (* ignore TPTP type information *)
         else if s = tptp_equal then
           let val ts = map (do_term [] NONE) us in
isabelle