# HG changeset patch
# User wenzelm
# Date 916155741 -3600
# Node ID 36f272ea94131fd656f0f164ca2283defd6fbc68
# Parent  b985e21848681719946ef590cdf3558dcf0da688
get_tthms witness theorems;

diff -r b985e2184868 -r 36f272ea9413 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jan 12 16:00:31 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 12 16:42:21 1999 +0100
@@ -31,18 +31,7 @@
        induction : thm,
        size : thm list,
        simps : thm 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 ->
+  val rep_datatype : string list option -> thm list list ->
     thm list list -> thm -> theory -> theory *
       {distinct : thm list list,
        inject : thm list list,
@@ -483,14 +472,10 @@
 
 (*********************** declare non-datatype as datatype *********************)
 
-fun gen_rep_datatype get get' alt_names distinct_names inject_names induction_name thy =
+fun rep_datatype alt_names distinct inject induction 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: " ^
@@ -571,8 +556,6 @@
       simps = simps})
   end;
 
-val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
-val rep_datatype_i = gen_rep_datatype (K I) (K I);
 
 (******************************** add datatype ********************************)
 
diff -r b985e2184868 -r 36f272ea9413 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue Jan 12 16:00:31 1999 +0100
+++ b/src/HOL/thy_syntax.ML	Tue Jan 12 16:42:21 1999 +0100
@@ -134,22 +134,25 @@
       ";\nlocal\n\
       \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
       \  case_thms, split_thms, induction, size, simps}) =\n\
-      \  DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
+      \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
       \in\n" ^ mk_bind_thms_string names ^
       "val thy = thy;\nend;\nval thy = thy\n"
     end;
 
+  fun mk_thmss namess = "(map (PureThy.get_thmss thy) " ^ mk_list (map mk_list namess) ^ ")";
+  fun mk_thm name = "(PureThy.get_thm thy " ^ name ^ ")";
+
   fun mk_rep_dt_string (((names, distinct), inject), induct) =
     ";\nlocal\n\
     \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
     \  case_thms, split_thms, induction, size, simps}) =\n\
-    \  DatatypePackage.rep_datatype " ^
+    \ DatatypePackage.rep_datatype " ^
     (case names of
-        Some names => "(Some [" ^ commas_quote names ^ "]) " ^
-          mk_list (map mk_list distinct) ^ " " ^ mk_list (map mk_list inject) ^
-            " " ^ induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
-      | None => "None " ^ mk_list (map mk_list distinct) ^ " " ^
-          mk_list (map mk_list inject) ^ " " ^ induct ^ " thy;\nin\n") ^
+        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
+          mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
+            "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
+      | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
+            "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
     "val thy = thy;\nend;\nval thy = thy\n";
 
   (*** parsers ***)