diff -r d0b190b4f15d -r bed899f14df7 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 19 14:47:53 2021 +0200
@@ -269,9 +269,9 @@
           val tm = do_term NONE term
         in quantify_over_var true lambda' var_name typ tm end
       | ATerm ((s, tys), us) =>
-        if s = ""
-        then error "Isar proof reconstruction failed because the ATP proof \
-                     \contains unparsable material"
+        if s = "" (* special marker generated on parse error *) then
+          error "Isar proof reconstruction failed because the ATP proof contains unparsable \
+            \material"
         else if s = tptp_equal then
           list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
             map (do_term NONE) us)
@@ -347,7 +347,7 @@
     fun do_term extra_ts opt_T u =
       (case u of
         ATerm ((s, tys), us) =>
-        if s = "" then
+        if s = "" (* special marker generated on parse error *) then
           error "Isar proof reconstruction failed because the ATP proof contains unparsable \
             \material"
         else if String.isPrefix native_type_prefix s then