src/HOL/Tools/datatype_abs_proofs.ML
changeset 5891 92e0f5e6fd17
parent 5661 6ecb6ea25f19
child 6092 d9db67970c73
--- 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;