# HG changeset patch
# User berghofe
# Date 1197912712 -3600
# Node ID 8b2ddc6e7be19243e447b2f368d529e045ea6156
# Parent  f3815084e89ebf7e86283f35232a7f11d1d1bcac
- Removed redundant head_len field in datatype_info
- Added new alt_names field in datatype_info

diff -r f3815084e89e -r 8b2ddc6e7be1 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Dec 17 18:30:44 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Dec 17 18:31:52 2007 +0100
@@ -456,12 +456,12 @@
 
 (**** make datatype info ****)
 
-fun make_dt_info head_len descr sorts induct reccomb_names rec_thms
+fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms
     (((((((((i, (_, (tname, _, _))), case_name), case_thms),
       exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
   (tname,
    {index = i,
-    head_len = head_len,
+    alt_names = alt_names,
     descr = descr,
     sorts = sorts,
     rec_names = reccomb_names,
@@ -620,8 +620,7 @@
     val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
       (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
 
-    val dt_infos = map (make_dt_info (length (hd descr)) descr' sorts induct
-        reccomb_names' rec_thms)
+    val dt_infos = map (make_dt_info NONE descr' sorts induct reccomb_names' rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
         exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
           nchotomys ~~ case_congs ~~ weak_case_congs);
@@ -680,8 +679,7 @@
     val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       descr sorts thy9;
 
-    val dt_infos = map (make_dt_info (length (hd descr)) (flat descr) sorts induct
-        reccomb_names rec_thms)
+    val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
         casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
@@ -781,8 +779,7 @@
       ||> Sign.add_path (space_implode "_" new_type_names)
       ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
 
-    val dt_infos = map (make_dt_info (length descr) descr sorts induction'
-        reccomb_names rec_thms)
+    val dt_infos = map (make_dt_info alt_names descr sorts induction' reccomb_names rec_thms)
       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
         map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);