# HG changeset patch
# User wenzelm
# Date 1393519160 -3600
# Node ID 8d4d339177dc19fe1687ff95ffe1155e88eec575
# Parent  67699e08e96916fb27121d5a7252590e7fe28b57
modernized theory setup;

diff -r 67699e08e969 -r 8d4d339177dc src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Feb 27 17:29:58 2014 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Feb 27 17:39:20 2014 +0100
@@ -183,6 +183,4 @@
 ML_file "Tools/spark_vcs.ML"
 ML_file "Tools/spark_commands.ML"
 
-setup SPARK_Commands.setup
-
 end
diff -r 67699e08e969 -r 8d4d339177dc src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Thu Feb 27 17:29:58 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Thu Feb 27 17:39:20 2014 +0100
@@ -4,13 +4,7 @@
 
 Isar commands for handling SPARK/Ada verification conditions.
 *)
-
-signature SPARK_COMMANDS =
-sig
-  val setup: theory -> theory
-end
-
-structure SPARK_Commands: SPARK_COMMANDS =
+structure SPARK_Commands: sig end =
 struct
 
 fun spark_open header (prfx, files) thy =
@@ -172,11 +166,11 @@
          (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
        (Toplevel.theory o SPARK_VCs.close));
 
-val setup = Theory.at_end (fn thy =>
+val _ = Theory.setup (Theory.at_end (fn thy =>
   let
     val _ = SPARK_VCs.is_closed thy
       orelse error ("Found the end of the theory, " ^ 
         "but the last SPARK environment is still open.")
-  in NONE end);
+  in NONE end));
 
 end;