--- a/src/HOL/Tools/inductive_codegen.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jan 19 21:22:08 2006 +0100
@@ -8,7 +8,7 @@
signature INDUCTIVE_CODEGEN =
sig
val add : string option -> theory attribute
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end;
structure InductiveCodegen : INDUCTIVE_CODEGEN =
@@ -732,10 +732,9 @@
| _ => NONE);
val setup =
- [add_codegen "inductive" inductive_codegen,
- CodegenData.init,
- add_attribute "ind"
- (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
+ add_codegen "inductive" inductive_codegen #>
+ CodegenData.init #>
+ add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
end;