Changed interface of rep_datatype: Characteristic theorems
of datatypes are now specified by xstrings.

--- a/src/HOL/Tools/datatype_package.ML	Wed Oct 21 17:53:16 1998 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Oct 21 17:55:18 1998 +0200
@@ -31,7 +31,18 @@
        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,
@@ -472,10 +483,14 @@
 
 (*********************** 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: " ^
@@ -556,6 +571,9 @@
       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 ********************************)