src/HOL/SPARK/Tools/spark_commands.ML

--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:24: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