src/HOL/Tools/inductive_package.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4      theory -> theory *
     1.5        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
     1.6         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.12 @@ -868,10 +868,10 @@
    1.13  (* setup theory *)
    1.14  
    1.15  val setup =
    1.16 - [InductiveData.init,
    1.17 +  InductiveData.init #>
    1.18    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
    1.19 -    "dynamic case analysis on sets")],
    1.20 -  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
    1.21 +    "dynamic case analysis on sets")] #>
    1.22 +  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
    1.23  
    1.24  
    1.25  (* outer syntax *)