src/ZF/Tools/induct_tacs.ML
changeset 18708 4b3dadb4fe33
parent 18688 abf0f018b5ec
child 18728 6790126ab5f6
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
     1.5    val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
     1.6      (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
     1.7 -  val setup: (theory -> theory) list
     1.8 +  val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -185,13 +185,13 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val setup =
    1.16 - [DatatypesData.init,
    1.17 -  ConstructorsData.init,
    1.18 + (DatatypesData.init #>
    1.19 +  ConstructorsData.init #>
    1.20    Method.add_methods
    1.21      [("induct_tac", Method.goal_args Args.name induct_tac,
    1.22        "induct_tac emulation (dynamic instantiation!)"),
    1.23       ("case_tac", Method.goal_args Args.name exhaust_tac,
    1.24 -      "datatype case_tac emulation (dynamic instantiation!)")]];
    1.25 +      "datatype case_tac emulation (dynamic instantiation!)")]);
    1.26  
    1.27  
    1.28  (* outer syntax *)