Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SPARK/Tools/spark_vcs.ML
changeset 66168 fcd09fc36d7f
parent 64574 1134e4d5e5b7
child 67522 9e712280cc37 
--- 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;
isabelle