--- 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, [])
--- 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