more modular setup;
authorwenzelm
Fri, 23 Aug 2013 12:43:16 +0200
changeset 53165 787d04a7c2d5
parent 53164 beb4ee344c22
child 53166 1266b6208a5b
more modular setup;
src/Tools/Spec_Check/Spec_Check.thy
src/Tools/Spec_Check/output_style.ML
--- 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
--- 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