# HG changeset patch
# User haftmann
# Date 1254075596 -7200
# Node ID 45929374f1bda71b85b09ff7dc15591d8195b6bd
# Parent  0e787c721fa3477423b857fa2191f9040a23f019
more appropriate order of field in dt_info

diff -r 0e787c721fa3 -r 45929374f1bd src/HOL/Tools/Datatype/datatype.ML
--- 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 *)
 
diff -r 0e787c721fa3 -r 45929374f1bd src/HOL/Tools/Datatype/datatype_aux.ML
--- 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);