Attribute.tthms_of;
authorwenzelm
Mon Nov 16 11:14:02 1998 +0100 (1998-11-16)
changeset 589192e0f5e6fd17
parent 5890 92ba560f39ab
child 5892 e5e44cc54eb2
Attribute.tthms_of;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
     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;
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Nov 16 11:13:28 1998 +0100
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Nov 16 11:14:02 1998 +0100
     2.3 @@ -78,7 +78,7 @@
     2.4  fun store_thmss label tnames thmss thy =
     2.5    foldr (fn ((tname, thms), thy') => thy' |>
     2.6      Theory.add_path tname |>
     2.7 -    PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
     2.8 +    PureThy.add_tthmss [((label, Attribute.tthms_of thms), [])] |>
     2.9      Theory.parent_path)
    2.10        (tnames ~~ thmss, thy);
    2.11  
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:13:28 1998 +0100
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Nov 16 11:14:02 1998 +0100
     3.3 @@ -464,9 +464,9 @@
     3.4        else standard (raw_induct RSN (2, rev_mp));
     3.5  
     3.6      val thy'' = thy' |>
     3.7 -      PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
     3.8 +      PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
     3.9        (if no_elim then I else PureThy.add_tthmss
    3.10 -        [(("elims", map Attribute.tthm_of elims), [])]) |>
    3.11 +        [(("elims", Attribute.tthms_of elims), [])]) |>
    3.12        (if no_ind then I else PureThy.add_tthms
    3.13          [(((if coind then "co" else "") ^ "induct",
    3.14            Attribute.tthm_of induct), [])]) |>
    3.15 @@ -600,8 +600,8 @@
    3.16      val intr_ts'' = map subst intr_ts';
    3.17  
    3.18    in add_inductive_i verbose false "" coind false false cs'' intr_ts''
    3.19 -    (map (Attribute.thm_of) (PureThy.get_tthmss thy monos))
    3.20 -    (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy
    3.21 +    (Attribute.thms_of (PureThy.get_tthmss thy monos))
    3.22 +    (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
    3.23    end;
    3.24  
    3.25  end;
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:13:28 1998 +0100
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:14:02 1998 +0100
     4.3 @@ -225,7 +225,7 @@
     4.4        commas names1 ^ " ...");
     4.5      val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
     4.6          (fn _ => [rtac refl 1])) eqns;
     4.7 -    val tsimps = map Attribute.tthm_of char_thms;
     4.8 +    val tsimps = Attribute.tthms_of char_thms;
     4.9      val thy'' = thy' |>
    4.10        PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
    4.11        PureThy.add_tthms (map (rpair [])