src/Tools/Code/code_target.ML

   val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
 
   val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
-
-  val setup: theory -> theory
 end;
 
 structure Code_Target : CODE_TARGET =
 struct
 

       val thy = Proof_Context.theory_of ctxt;
     in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
 
 in
 
-val antiq_setup =
-  Thy_Output.antiquotation @{binding code_stmts}
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding code_stmts}
     (parse_const_terms --
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
     (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
         present_code ctxt (mk_cs ctxt)
           (maps (fn f => f ctxt) mk_stmtss)
-          target_name some_width "Example" []);
+          target_name some_width "Example" []));
 
 end;
 
 
 (** serializer configuration **)

   in case parse cmd_expr
    of SOME f => (writeln "Now generating code..."; f ctxt)
     | NONE => error ("Bad directive " ^ quote cmd_expr)
   end;
 
-
-(** theory setup **)
-
-val setup = antiq_setup;
-
 end; (*struct*)