src/HOL/Tools/datatype_package.ML

   end;
 
 
 (**** 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,
     rec_rewrites = rec_thms,
     case_name = case_name,

     val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names
       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
     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);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;

     val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
       descr sorts nchotomys case_thms thy8;
     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);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
 

       |> store_thmss "inject" new_type_names inject
       ||>> store_thmss "distinct" new_type_names distinct
       ||> 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);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;