src/HOL/SPARK/Tools/spark_commands.ML

--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -61,7 +61,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 true lthy
   end;
 
 fun string_of_status NONE = "(unproved)"