src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32718 45929374f1bd
parent 32712 ec5976f4d3d8
child 32727 9072201cd69d
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 20:15:45 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 20:19:56 2009 +0200
     1.3 @@ -191,18 +191,18 @@
     1.4     alt_names : string list option,
     1.5     descr : descr,
     1.6     sorts : (string * sort) list,
     1.7 +   inject : thm list,
     1.8 +   distinct : simproc_dist,
     1.9 +   inducts : thm list * thm,
    1.10 +   exhaust : thm,
    1.11 +   nchotomy : thm,
    1.12     rec_names : string list,
    1.13     rec_rewrites : thm list,
    1.14     case_name : string,
    1.15     case_rewrites : thm list,
    1.16 -   inducts : thm list * thm,
    1.17 -   exhaust : thm,
    1.18 -   distinct : simproc_dist,
    1.19 -   inject : thm list,
    1.20 -   splits : thm * thm,
    1.21 -   nchotomy : thm,
    1.22     case_cong : thm,
    1.23 -   weak_case_cong : thm};
    1.24 +   weak_case_cong : thm,
    1.25 +   splits : thm * thm};
    1.26  
    1.27  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
    1.28