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 ***)