src/HOL/SPARK/Tools/spark_commands.ML

 fun prove_vc vc_name lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val (ctxt, stmt) = get_vc thy vc_name
   in
-    Specification.theorem Thm.theoremK NONE
+    Specification.theorem true Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
       (Binding.name vc_name, []) [] ctxt stmt false lthy
   end;