diff -r a2e9af953b90 -r 582cccdda0ed src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 04 11:43:20 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 04 17:39:30 2011 +0100
@@ -45,7 +45,7 @@
 fun get_vc thy vc_name =
   (case SPARK_VCs.lookup_vc thy vc_name of
     SOME (ctxt, (_, proved, ctxt', stmt)) =>
-      if proved then
+      if is_some proved then
         error ("The verification condition " ^
           quote vc_name ^ " has already been proved.")
       else (ctxt @ [ctxt'], stmt)
@@ -58,12 +58,13 @@
     val (ctxt, stmt) = get_vc thy vc_name
   in
     Specification.theorem Thm.theoremK NONE
-      (K (Local_Theory.background_theory (SPARK_VCs.mark_proved vc_name)))
+      (fn thmss => (Local_Theory.background_theory
+         (SPARK_VCs.mark_proved vc_name (flat thmss))))
       (Binding.name vc_name, []) ctxt stmt true lthy
   end;
 
-fun string_of_status false = "(unproved)"
-  | string_of_status true = "(proved)";
+fun string_of_status NONE = "(unproved)"
+  | string_of_status (SOME _) = "(proved)";
 
 fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
   let
@@ -131,8 +132,8 @@
     Keyword.diag
     (Scan.optional
        (Args.parens
-          (   Args.$$$ "proved" >> K (I, K "")
-           || Args.$$$ "unproved" >> K (not, K "")))
+          (   Args.$$$ "proved" >> K (is_some, K "")
+           || Args.$$$ "unproved" >> K (is_none, K "")))
        (K true, string_of_status) >> show_status);
 
 val _ =