diff -r a265e41cc33b -r ddd3af5a683d src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun May 04 19:08:29 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun May 04 19:27:28 2014 +0200
@@ -496,7 +496,8 @@
 
 fun repair_waldmeister_endgame proof =
   let
-    fun repair_tail (name, _, t, rule, deps) = (name, Negated_Conjecture, s_not t, rule, deps)
+    fun repair_tail (name, _, @{const Trueprop} $ t, rule, deps) =
+      (name, Negated_Conjecture, @{const Trueprop} $ s_not t, rule, deps)
     fun repair_body [] = []
       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)