1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -963,7 +963,7 @@
     1.4            val (proved, unproved) = partition_vcs vcs;
     1.5            val _ = Thm.join_proofs (maps (#2 o snd) proved);
     1.6            val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
     1.7 -            exists (#oracle o Thm.status_of) thms) proved
     1.8 +            exists (#oracle o Thm.peek_status) thms) proved
     1.9          in
    1.10            (if null unproved then ()
    1.11             else (if incomplete then warning else error)