# HG changeset patch
# User smolkas
# Date 1367830988 -7200
# Node ID f11039b31bae22e905feb08e98f88487550e297a
# Parent  71052c42edf22ea9679f74271af36c3dafe0f5a0
handle dummy atp terms

diff -r 71052c42edf2 -r f11039b31bae src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon May 06 11:03:08 2013 +0200
@@ -265,7 +265,7 @@
 fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal)
 fun is_built_in_tptp_symbol s =
   s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0)))
-fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
+fun is_tptp_variable s = s <> "" andalso Char.isUpper (String.sub (s, 0))
 val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
 
 val bool_atype = AType (`I tptp_bool_type, [])
diff -r 71052c42edf2 -r f11039b31bae src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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