# HG changeset patch
# User haftmann
# Date 1400164709 -7200
# Node ID a3f911785efaf9128350017e350f20bad61ba5f2
# Parent  7491932da5743dfde2b7e461ec48f14e5eedb3a4
modernized setup

diff -r 7491932da574 -r a3f911785efa src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
@@ -32,8 +32,6 @@
   val static_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> string list
     -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
     -> Proof.context -> term -> 'b
-
-  val setup: theory -> theory
 end
 
 structure Code_Preproc : CODE_PREPROC =
@@ -507,19 +505,20 @@
 
 (** setup **)
 
-val setup = 
+val _ =
   let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     fun add_del_attribute_parser process =
       Attrib.add_del (mk_attribute (process Simplifier.add_simp))
         (mk_attribute (process Simplifier.del_simp));
   in
-    Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
+    Context.>> (Context.map_theory
+      (Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
         "preprocessing equations for code generator"
-    #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
+      #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
         "postprocessing equations for code generator"
-    #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
-        "post- and preprocessing equations for code generator"
+      #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
+        "post- and preprocessing equations for code generator"))
   end;
 
 val _ =
diff -r 7491932da574 -r a3f911785efa src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu May 15 16:38:29 2014 +0200
+++ b/src/Tools/Code_Generator.thy	Thu May 15 16:38:29 2014 +0200
@@ -27,8 +27,7 @@
 ML_file "~~/src/Tools/Code/code_scala.ML"
 
 setup {*
-  Code_Preproc.setup
-  #> Code_Simp.setup
+  Code_Simp.setup
   #> Code_Target.setup
   #> Code_ML.setup
   #> Code_Haskell.setup