diff -r 3081f7719df7 -r 056ea294c256 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 13:52:01 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat May 14 19:49:10 2016 +0200
@@ -48,7 +48,7 @@
     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