diff -r dfc834e39c1f -r fefe3ea75289 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:11 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:11 2014 +0200
@@ -232,11 +232,25 @@
         then error "Isar proof reconstruction failed because the ATP proof \
                      \contains unparsable material."
         else if s = tptp_equal then
-          let val ts = map (do_term NONE) us in
-            if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
-              @{const True}
+          let
+            val ts = map (do_term NONE) us
+            fun equal_term ts =
+                list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
+          in
+            if textual then
+              (case ts of
+                [fst, lst] =>
+                if loose_aconv (fst, lst) then
+                  @{const True}
+                else if Term.aconv_untyped (lst, @{const True}) then
+                  fst
+                else if Term.aconv_untyped (fst, @{const True}) then
+                  lst
+                else
+                  equal_term ts
+              | _ => equal_term ts)
             else
-              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
+              equal_term ts
           end
         else if not (null us) then
           let