diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Apr 21 22:00:28 2005 +0200
+++ b/src/Pure/codegen.ML	Thu Apr 21 22:02:06 2005 +0200
@@ -55,8 +55,6 @@
   val test_fn: (int -> (string * term) list option) ref
   val test_term: theory -> int -> int -> term -> (string * term) list option
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
-  val parsers: OuterSyntax.parser list
-  val setup: (theory -> theory) list
 end;
 
 structure Codegen : CODEGEN =
@@ -169,6 +167,7 @@
 end;
 
 structure CodegenData = TheoryDataFun(CodegenArgs);
+val _ = Context.add_setup [CodegenData.init];
 val print_codegens = CodegenData.print;
 
 
@@ -228,6 +227,11 @@
   Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
     (#attrs (CodegenData.get thy)))));
 
+val _ = Context.add_setup
+ [Attrib.add_attributes
+  [("code", (code_attr, K Attrib.undef_local_attribute),
+     "declare theorems for code generation")]];
+
 
 (**** preprocessors ****)
 
@@ -254,6 +258,8 @@
       else th)
   in (add_preprocessor prep thy, eqn) end;
 
+val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
+
 
 (**** associate constants with target language code ****)
 
@@ -287,6 +293,7 @@
 val assoc_consts_i = gen_assoc_consts (K I);
 val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
 
+
 (**** associate types with target language types ****)
 
 fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
@@ -553,6 +560,10 @@
                (invoke_tycodegen thy dep false) (gr', quotes_of ms)
            in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end);
 
+val _ = Context.add_setup
+ [add_codegen "default" default_codegen,
+  add_tycodegen "default" default_tycodegen];
+
 
 fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   (rev (Graph.all_preds gr xs)));
@@ -698,6 +709,10 @@
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
 
+val _ = Context.add_setup
+  [assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]];
+
+
 structure P = OuterParse and K = OuterSyntax.Keyword;
 
 val assoc_typeP =
@@ -761,18 +776,7 @@
           (map (fn f => f (Toplevel.sign_of st))) ps, []))
         (get_test_params (Toplevel.theory_of st), [])) g st)));
 
-val parsers = [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
-
-val setup =
-  [CodegenData.init,
-   add_codegen "default" default_codegen,
-   add_tycodegen "default" default_tycodegen,
-   assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")],
-   Attrib.add_attributes [("code",
-     (code_attr, K Attrib.undef_local_attribute),
-     "declare theorems for code generation")],
-   add_attribute "unfold" (Scan.succeed unfold_attr)];
+val _ = OuterSyntax.add_parsers
+  [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
 
 end;
-
-OuterSyntax.add_parsers Codegen.parsers;