src/HOL/Tools/Datatype/datatype.ML
changeset 32718 45929374f1bd
parent 32717 0e787c721fa3
child 32719 36cae240b46c
     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