src/HOL/Tools/typedef_package.ML

       Rep_induct: thm, Abs_induct: thm}
   val typedef: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
-  val setup: (theory -> theory) list
+  val setup: theory -> theory
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
 struct
 

              | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
            end)
   | typedef_tycodegen thy defs gr dep module brack _ = NONE;
 
 val setup =
-  [TypedefData.init,
-   Codegen.add_codegen "typedef" typedef_codegen,
-   Codegen.add_tycodegen "typedef" typedef_tycodegen];
+  TypedefData.init #>
+  Codegen.add_codegen "typedef" typedef_codegen #>
+  Codegen.add_tycodegen "typedef" typedef_tycodegen;
 
 
 
 (** outer syntax **)