# 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;