more appropriate order of field in dt_info
authorhaftmann
Sun Sep 27 20:19:56 2009 +0200 (2009-09-27 ago)
changeset 3271845929374f1bd
parent 32717 0e787c721fa3
child 32719 36cae240b46c
more appropriate order of field in dt_info
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:15:45 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:19:56 2009 +0200
     1.3 @@ -226,18 +226,18 @@
     1.4      alt_names = alt_names,
     1.5      descr = descr,
     1.6      sorts = sorts,
     1.7 +    inject = inject,
     1.8 +    distinct = distinct_thm,
     1.9 +    inducts = inducts,
    1.10 +    exhaust = exhaust_thm,
    1.11 +    nchotomy = nchotomy,
    1.12      rec_names = reccomb_names,
    1.13      rec_rewrites = rec_thms,
    1.14      case_name = case_name,
    1.15      case_rewrites = case_thms,
    1.16 -    inducts = inducts,
    1.17 -    exhaust = exhaust_thm,
    1.18 -    distinct = distinct_thm,
    1.19 -    inject = inject,
    1.20 -    splits = splits,
    1.21 -    nchotomy = nchotomy,
    1.22      case_cong = case_cong,
    1.23 -    weak_case_cong = weak_case_cong});
    1.24 +    weak_case_cong = weak_case_cong,
    1.25 +    splits = splits});
    1.26  
    1.27  (* case names *)
    1.28  
     2.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 20:15:45 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 20:19:56 2009 +0200
     2.3 @@ -191,18 +191,18 @@
     2.4     alt_names : string list option,
     2.5     descr : descr,
     2.6     sorts : (string * sort) list,
     2.7 +   inject : thm list,
     2.8 +   distinct : simproc_dist,
     2.9 +   inducts : thm list * thm,
    2.10 +   exhaust : thm,
    2.11 +   nchotomy : thm,
    2.12     rec_names : string list,
    2.13     rec_rewrites : thm list,
    2.14     case_name : string,
    2.15     case_rewrites : thm list,
    2.16 -   inducts : thm list * thm,
    2.17 -   exhaust : thm,
    2.18 -   distinct : simproc_dist,
    2.19 -   inject : thm list,
    2.20 -   splits : thm * thm,
    2.21 -   nchotomy : thm,
    2.22     case_cong : thm,
    2.23 -   weak_case_cong : thm};
    2.24 +   weak_case_cong : thm,
    2.25 +   splits : thm * thm};
    2.26  
    2.27  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
    2.28