# HG changeset patch
# User wenzelm
# Date 1377254596 -7200
# Node ID 787d04a7c2d53857937812a4f68db10f803316e1
# Parent  beb4ee344c229f90cc03892fc4f5632441c0428e
more modular setup;

diff -r beb4ee344c22 -r 787d04a7c2d5 src/Tools/Spec_Check/Spec_Check.thy
--- a/src/Tools/Spec_Check/Spec_Check.thy	Fri Aug 23 12:40:55 2013 +0200
+++ b/src/Tools/Spec_Check/Spec_Check.thy	Fri Aug 23 12:43:16 2013 +0200
@@ -9,6 +9,5 @@
 ML_file "gen_construction.ML"
 ML_file "spec_check.ML"
 ML_file "output_style.ML"
-setup Output_Style.setup
 
 end
\ No newline at end of file
diff -r beb4ee344c22 -r 787d04a7c2d5 src/Tools/Spec_Check/output_style.ML
--- a/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 12:40:55 2013 +0200
+++ b/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 12:43:16 2013 +0200
@@ -5,12 +5,7 @@
 Output styles for presenting Spec_Check's results.
 *)
 
-signature OUTPUT_STYLE =
-sig
-  val setup : theory -> theory
-end
-
-structure Output_Style : OUTPUT_STYLE =
+structure Output_Style : sig end =
 struct
 
 (* perl style *)
@@ -114,6 +109,6 @@
 
 (* setup *)
 
-val setup = perl_style #> cm_style
+val _ = Context.>> (Context.map_theory (perl_style #> cm_style));
 
 end