src/HOL/Tools/inductive_package.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
--- a/src/HOL/Tools/inductive_package.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -55,7 +55,7 @@
     theory -> theory *
       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
-  val setup: (theory -> theory) list
+  val setup: theory -> theory
 end;
 
 structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -868,10 +868,10 @@
 (* setup theory *)
 
 val setup =
- [InductiveData.init,
+  InductiveData.init #>
   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
-    "dynamic case analysis on sets")],
-  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
+    "dynamic case analysis on sets")] #>
+  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
 
 
 (* outer syntax *)