# HG changeset patch
# User wenzelm
# Date 911211284 -3600
# Node ID e5e44cc54eb2fc13f2d10b15587d0d5562de5446
# Parent  92e0f5e6fd17b21b0d28c5e5f9d61a23947d9a6c
Attribute.tthms_of;
Theory.copy;

diff -r 92e0f5e6fd17 -r e5e44cc54eb2 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Nov 16 11:14:02 1998 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Nov 16 11:14:44 1998 +0100
@@ -402,7 +402,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -459,7 +459,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -550,7 +550,7 @@
 
     val thy9 = thy8 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -572,7 +572,7 @@
   end;
 
 val rep_datatype = gen_rep_datatype
-  (fn thy => map Attribute.thm_of o PureThy.get_tthmss thy) get_thm;
+  (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm;
 val rep_datatype_i = gen_rep_datatype (K I) (K I);
 
 (******************************** add datatype ********************************)
@@ -584,7 +584,7 @@
     (* this theory is used just for parsing *)
 
     val tmp_thy = thy |>
-      Theory.prep_ext |>
+      Theory.copy |>
       Theory.add_types (map (fn (tvs, tname, mx, _) =>
         (tname, length tvs, mx)) dts);