--- a/src/ZF/Tools/induct_tacs.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Thu Jan 19 21:22:08 2006 +0100
@@ -15,7 +15,7 @@
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
(thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
@@ -185,13 +185,13 @@
(* theory setup *)
val setup =
- [DatatypesData.init,
- ConstructorsData.init,
+ (DatatypesData.init #>
+ ConstructorsData.init #>
Method.add_methods
[("induct_tac", Method.goal_args Args.name induct_tac,
"induct_tac emulation (dynamic instantiation!)"),
("case_tac", Method.goal_args Args.name exhaust_tac,
- "datatype case_tac emulation (dynamic instantiation!)")]];
+ "datatype case_tac emulation (dynamic instantiation!)")]);
(* outer syntax *)