src/HOL/Nominal/nominal_datatype.ML

 
 
 (**** make datatype info ****)
 
 fun make_dt_info descr sorts induct reccomb_names rec_thms
-    (((i, (_, (tname, _, _))), distinct), inject) =
+    (i, (((_, (tname, _, _)), distinct), inject)) =
   (tname,
    {index = i,
     descr = descr,
     sorts = sorts,
     rec_names = reccomb_names,

              resolve_tac rec_intrs 1,
              REPEAT (solve (prems @ rec_total_thms) prems 1)])
       end) (rec_eq_prems ~~
         DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
 
-    val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
-      ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
+    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+      (descr1 ~~ distinct_thms ~~ inject_thms);
 
     (* FIXME: theorems are stored in database for testing only *)
     val (_, thy13) = thy12 |>
       PureThy.add_thmss
         [((Binding.name "rec_equiv", flat rec_equiv_thms), []),