# HG changeset patch
# User wenzelm
# Date 1566055688 -7200
# Node ID fb3d06d7dd05c1eb8b913e8e5bf0deb7345952af
# Parent  d0b75c59beca26697ec4fb39553c8c72c975ee6b
more thorough check, using full dependency graph of finished proofs;

diff -r d0b75c59beca -r fb3d06d7dd05 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Aug 17 17:21:30 2019 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Aug 17 17:28:08 2019 +0200
@@ -961,8 +961,7 @@
           val (proved, unproved) = partition_vcs vcs;
           val _ = Thm.consolidate (maps (#2 o snd) proved);
           val (proved', proved'') =
-            List.partition (fn (_, (_, thms, _, _)) =>
-              exists (#oracle o Thm.peek_status) thms) proved;
+            List.partition (fn (_, (_, thms, _, _)) => Thm_Deps.has_skip_proof thms) proved;
           val _ =
             if null unproved then ()
             else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved));
diff -r d0b75c59beca -r fb3d06d7dd05 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 17 17:21:30 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 17 17:28:08 2019 +0200
@@ -8,6 +8,7 @@
 signature THM_DEPS =
 sig
   val all_oracles: thm list -> Proofterm.oracle list
+  val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
   val thm_deps: theory -> thm list -> unit
   val unused_thms: theory list * theory list -> (string * thm) list
@@ -21,6 +22,9 @@
 fun all_oracles thms =
   Proofterm.all_oracles_of (map Thm.proof_body_of thms);
 
+fun has_skip_proof thms =
+  all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>);
+
 fun pretty_thm_oracles ctxt thms =
   let
     fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]