src/HOL/Tools/datatype_package.ML
changeset 11345 cd605c85e421
parent 10930 7c7a7b0e1d0c
child 11539 0f17da240450
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu May 31 16:52:02 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu May 31 16:52:20 2001 +0200
     1.3 @@ -285,6 +285,15 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +fun add_rules simps case_thms size_thms rec_thms inject distinct
     1.8 +                  weak_case_congs cong_att =
     1.9 +  (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.10 +    (("", flat case_thms @ size_thms @ 
    1.11 +          flat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    1.12 +    (("", flat inject),               [iff_add_global]),
    1.13 +    (("", flat distinct RL [notE]),   [Classical.safe_elim_global]),
    1.14 +    (("", weak_case_congs),           [cong_att])]);
    1.15 +
    1.16  
    1.17  (* add_cases_induct *)
    1.18  
    1.19 @@ -570,10 +579,8 @@
    1.20  
    1.21      val thy12 = thy11 |>
    1.22        Theory.add_path (space_implode "_" new_type_names) |>
    1.23 -      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.24 -        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.25 -        (("", flat (inject @ distinct)), [iff_add_global]),
    1.26 -        (("", weak_case_congs), [Simplifier.cong_add_global])]) |>
    1.27 +      add_rules simps case_thms size_thms rec_thms inject distinct
    1.28 +                weak_case_congs Simplifier.cong_add_global |> 
    1.29        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.30        add_cases_induct dt_infos |>
    1.31        Theory.parent_path |>
    1.32 @@ -628,10 +635,8 @@
    1.33  
    1.34      val thy12 = thy11 |>
    1.35        Theory.add_path (space_implode "_" new_type_names) |>
    1.36 -      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.37 -        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.38 -        (("", flat (inject @ distinct)), [iff_add_global]),
    1.39 -        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    1.40 +      add_rules simps case_thms size_thms rec_thms inject distinct
    1.41 +                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.42        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.43        add_cases_induct dt_infos |>
    1.44        Theory.parent_path |>
    1.45 @@ -734,10 +739,8 @@
    1.46      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.47  
    1.48      val thy11 = thy10 |>
    1.49 -      (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.50 -        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.51 -        (("", flat (inject @ distinct)), [iff_add_global]),
    1.52 -        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    1.53 +      add_rules simps case_thms size_thms rec_thms inject distinct
    1.54 +                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.55        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.56        add_cases_induct dt_infos |>
    1.57        Theory.parent_path |>