--- a/src/HOL/Tools/Datatype/datatype.ML Sun Sep 27 20:15:45 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Sep 27 20:19:56 2009 +0200
@@ -226,18 +226,18 @@
alt_names = alt_names,
descr = descr,
sorts = sorts,
+ inject = inject,
+ distinct = distinct_thm,
+ inducts = inducts,
+ exhaust = exhaust_thm,
+ nchotomy = nchotomy,
rec_names = reccomb_names,
rec_rewrites = rec_thms,
case_name = case_name,
case_rewrites = case_thms,
- inducts = inducts,
- exhaust = exhaust_thm,
- distinct = distinct_thm,
- inject = inject,
- splits = splits,
- nchotomy = nchotomy,
case_cong = case_cong,
- weak_case_cong = weak_case_cong});
+ weak_case_cong = weak_case_cong,
+ splits = splits});
(* case names *)
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Sun Sep 27 20:15:45 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sun Sep 27 20:19:56 2009 +0200
@@ -191,18 +191,18 @@
alt_names : string list option,
descr : descr,
sorts : (string * sort) list,
+ inject : thm list,
+ distinct : simproc_dist,
+ inducts : thm list * thm,
+ exhaust : thm,
+ nchotomy : thm,
rec_names : string list,
rec_rewrites : thm list,
case_name : string,
case_rewrites : thm list,
- inducts : thm list * thm,
- exhaust : thm,
- distinct : simproc_dist,
- inject : thm list,
- splits : thm * thm,
- nchotomy : thm,
case_cong : thm,
- weak_case_cong : thm};
+ weak_case_cong : thm,
+ splits : thm * thm};
fun mk_Free s T i = Free (s ^ (string_of_int i), T);