diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/verit_proof_parse.ML
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Sat Apr 25 09:48:06 2015 +0200
@@ -70,7 +70,7 @@
     val fact_helper_ids' =
       map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
   in
-    {outcome = NONE, fact_ids = fact_ids',
+    {outcome = NONE, fact_ids = SOME fact_ids',
      atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
        fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
   end