src/Pure/codegen.ML

   val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
   val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
   val mk_deftab: theory -> deftab
   val add_unfold: thm -> theory -> theory
 
+  val setup: theory -> theory
+
   val get_node: codegr -> string -> node
   val add_edge: string * string -> codegr -> codegr
   val add_edge_acyclic: string * string -> codegr -> codegr
   val del_nodes: string list -> codegr -> codegr
   val map_node: string -> (node -> node) -> codegr -> codegr

         then rewrite_rule [eqn'] (Thm.transfer thy th)
         else th
       end)
   in add_preprocessor prep end;
 
-val _ = Context.add_setup
-  (let
-    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-  in
-    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
-      (fn thm => add_unfold thm #> Code.add_inline thm)))
-  end);
 
 
 (**** associate constants with target language code ****)
 
 fun gen_assoc_const prep_const (raw_const, syn) thy =

                      p module'))
              | SOME (_, module'', _) =>
                  (add_edge (node_id, dep) gr'', p module''))
            end);
 
-val _ = Context.add_setup
- (add_codegen "default" default_codegen #>
-  add_tycodegen "default" default_tycodegen);
-
-
 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
 
 fun add_to_module name s = AList.map_entry (op =) name (suffix s);
 
 fun output_code gr module xs =

 fun evaluation_oracle (thy, Evaluation t) =
   Logic.mk_equals (t, eval_term thy t);
 
 fun evaluation_conv ct =
   let val {thy, t, ...} = rep_cterm ct
-  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
-
-val _ = Context.add_setup
-  (Theory.add_oracle ("evaluation", evaluation_oracle));
+  in Thm.invoke_oracle_i thy "Code_Setup.evaluation" (thy, Evaluation t) end;
+
 
 (**** Interface ****)
 
 val str = PrintMode.with_default Pretty.str;
 

             || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
                  (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
        (Symbol.explode s) of
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
-
-val _ = Context.add_setup
-  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
-     [("term_of",
-       "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
-      ("test",
-       "fun gen_fun_type _ G i =\n\
-       \  let\n\
-       \    val f = ref (fn x => raise Match);\n\
-       \    val _ = (f := (fn x =>\n\
-       \      let\n\
-       \        val y = G i;\n\
-       \        val f' = !f\n\
-       \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
-       \  in (fn x => !f x) end;\n")]))]);
 
 
 structure P = OuterParse and K = OuterKeyword;
 
 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")

 val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
 
 val _ = OuterSyntax.add_parsers
   [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
 
+val setup = 
+  let
+    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+  in
+    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
+      (fn thm => add_unfold thm #> Code.add_inline thm)))
+    #> add_codegen "default" default_codegen
+    #> add_tycodegen "default" default_tycodegen
+    #> Theory.add_oracle ("evaluation", evaluation_oracle)
+    #> fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
+        [("term_of",
+            "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
+        ("test",
+           "fun gen_fun_type _ G i =\n\
+           \  let\n\
+           \    val f = ref (fn x => raise Match);\n\
+           \    val _ = (f := (fn x =>\n\
+           \      let\n\
+           \        val y = G i;\n\
+           \        val f' = !f\n\
+           \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
+           \  in (fn x => !f x) end;\n")]))]
+  end;
+
 end;