# HG changeset patch
# User wenzelm
# Date 1428178958 -7200
# Node ID 251fa1530de151a6f52c0e3dc6a94e3c13787605
# Parent  003dbac78546bc7032777edbfc76579523d3506d
more standard local_theory command setup;

diff -r 003dbac78546 -r 251fa1530de1 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sat Apr 04 22:01:30 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat Apr 04 22:22:38 2015 +0200
@@ -121,9 +121,9 @@
        (Toplevel.theory o fold add_spark_type_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_spec "spark_vc"}
+  Outer_Syntax.local_theory_to_proof @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE NONE (prove_vc name)));
+    (Parse.name >> prove_vc);
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_status"}