diff -r fa12200276bf -r f058120aaad4 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 12:59:15 2014 +0200
@@ -123,8 +123,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    (Parse.name >> (fn name =>
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
+    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "spark_status"}