Attribute.tthms_of;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Nov 16 11:13:28 1998 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Nov 16 11:14:02 1998 +0100
@@ -275,7 +275,7 @@
 
   in
     (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
-             PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] |>
+             PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |>
              Theory.parent_path,
      reccomb_names, rec_thms)
   end;
@@ -518,7 +518,7 @@
 
   in
     (thy' |> Theory.add_path big_name |>
-             PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] |>
+             PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |>
              Theory.parent_path,
      size_thms)
   end;

--- a/src/HOL/Tools/datatype_aux.ML	Mon Nov 16 11:13:28 1998 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Nov 16 11:14:02 1998 +0100
@@ -78,7 +78,7 @@
 fun store_thmss label tnames thmss thy =
   foldr (fn ((tname, thms), thy') => thy' |>
     Theory.add_path tname |>
-    PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
+    PureThy.add_tthmss [((label, Attribute.tthms_of thms), [])] |>
     Theory.parent_path)
       (tnames ~~ thmss, thy);
 

--- a/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:13:28 1998 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:14:02 1998 +0100
@@ -464,9 +464,9 @@
       else standard (raw_induct RSN (2, rev_mp));
 
     val thy'' = thy' |>
-      PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
+      PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
       (if no_elim then I else PureThy.add_tthmss
-        [(("elims", map Attribute.tthm_of elims), [])]) |>
+        [(("elims", Attribute.tthms_of elims), [])]) |>
       (if no_ind then I else PureThy.add_tthms
         [(((if coind then "co" else "") ^ "induct",
           Attribute.tthm_of induct), [])]) |>
@@ -600,8 +600,8 @@
     val intr_ts'' = map subst intr_ts';
 
   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
-    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
-    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
+    (Attribute.thms_of (PureThy.get_tthmss thy monos))
+    (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
   end;
 
 end;

--- a/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:13:28 1998 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:14:02 1998 +0100
@@ -225,7 +225,7 @@
       commas names1 ^ " ...");
     val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
         (fn _ => [rtac refl 1])) eqns;
-    val tsimps = map Attribute.tthm_of char_thms;
+    val tsimps = Attribute.tthms_of char_thms;
     val thy'' = thy' |>
       PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
       PureThy.add_tthms (map (rpair [])