src/HOL/Tools/datatype_package.ML

        case_thms : thm list list,
        split_thms : (thm * thm) list,
        induction : thm,
        size : thm list,
        simps : thm list}
-  val add_rep_datatype : string list option -> thm list list ->
+  val rep_datatype : string list option -> xstring list list ->
+    xstring list list -> xstring -> theory -> theory *
+      {distinct : thm list list,
+       inject : thm list list,
+       exhaustion : thm list,
+       rec_thms : thm list,
+       case_thms : thm list list,
+       split_thms : (thm * thm) list,
+       induction : thm,
+       size : thm list,
+       simps : thm list}
+  val rep_datatype_i : string list option -> thm list list ->
     thm list list -> thm -> theory -> theory *
       {distinct : thm list list,
        inject : thm list list,
        exhaustion : thm list,
        rec_thms : thm list,

   end;
 
 
 (*********************** declare non-datatype as datatype *********************)
 
-fun add_rep_datatype alt_names distinct inject induction thy =
+fun gen_rep_datatype get get' alt_names distinct_names inject_names induction_name thy =
   let
     val sign = sign_of thy;
+
+    val distinct = map (get thy) distinct_names;
+    val inject = map (get thy) inject_names;
+    val induction = get' thy induction_name;
 
     val induction' = freezeT induction;
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term sign t);

       induction = induction,
       size = size_thms,
       simps = simps})
   end;
 
+val rep_datatype = gen_rep_datatype
+  (fn thy => map Attribute.thm_of o PureThy.get_tthmss thy) get_thm;
+val rep_datatype_i = gen_rep_datatype (K I) (K I);
 
 (******************************** add datatype ********************************)
 
 fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
   let