src/HOL/Tools/datatype_abs_proofs.ML
changeset 5891 92e0f5e6fd17
parent 5661 6ecb6ea25f19
child 6092 d9db67970c73
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Nov 16 11:13:28 1998 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Nov 16 11:14:02 1998 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4  
     1.5    in
     1.6      (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
     1.7 -             PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] |>
     1.8 +             PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |>
     1.9               Theory.parent_path,
    1.10       reccomb_names, rec_thms)
    1.11    end;
    1.12 @@ -518,7 +518,7 @@
    1.13  
    1.14    in
    1.15      (thy' |> Theory.add_path big_name |>
    1.16 -             PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] |>
    1.17 +             PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |>
    1.18               Theory.parent_path,
    1.19       size_thms)
    1.20    end;