diff -r af8ecf09a58c -r 065c684130ad src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Jan 09 20:46:32 2013 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Jan 08 22:10:02 2013 +0100
@@ -75,7 +75,7 @@
     Specification.theorem Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
-      (Binding.name vc_name, []) [] ctxt stmt true lthy
+      (Binding.name vc_name, []) [] ctxt stmt false lthy
   end;
 
 fun string_of_status NONE = "(unproved)"