--- a/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -402,7 +402,7 @@
val thy11 = thy10 |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", 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", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", 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", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
@@ -571,8 +571,7 @@
simps = simps})
end;
-val rep_datatype = gen_rep_datatype
- (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm;
+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 ********************************)