diff -r 1bd268ab885c -r fcd09fc36d7f src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 15:20:32 2017 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 21:10:13 2017 +0200
@@ -959,7 +959,7 @@
     | SOME {vcs, path, ...} =>
         let
           val (proved, unproved) = partition_vcs vcs;
-          val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
+          val _ = Thm.consolidate (maps (#2 o snd) proved);
           val (proved', proved'') =
             List.partition (fn (_, (_, thms, _, _)) =>
               exists (#oracle o Thm.peek_status) thms) proved;