1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Jan 09 20:46:32 2013 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Jan 08 22:10:02 2013 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4      Specification.theorem Thm.theoremK NONE
     1.5        (fn thmss => (Local_Theory.background_theory
     1.6           (SPARK_VCs.mark_proved vc_name (flat thmss))))
     1.7 -      (Binding.name vc_name, []) [] ctxt stmt true lthy
     1.8 +      (Binding.name vc_name, []) [] ctxt stmt false lthy
     1.9    end;
    1.10  
    1.11  fun string_of_status NONE = "(unproved)"