src/HOL/Tools/datatype_package.ML
changeset 18688 abf0f018b5ec
parent 18678 dd0c569fa43d
child 18690 16a64bdc5485
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -350,10 +350,10 @@
     1.4                    weak_case_congs cong_att =
     1.5    (snd o PureThy.add_thmss [(("simps", simps), []),
     1.6      (("", List.concat case_thms @ size_thms @ 
     1.7 -          List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
     1.8 +          List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
     1.9      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    1.10 -    (("", List.concat inject),               [iff_add_global]),
    1.11 -    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim_global]),
    1.12 +    (("", List.concat inject),               [Attrib.theory iff_add]),
    1.13 +    (("", map name_notE (List.concat distinct)),  [Attrib.theory Classical.safe_elim]),
    1.14      (("", weak_case_congs),                  [cong_att])]);
    1.15  
    1.16  
    1.17 @@ -747,7 +747,7 @@
    1.18        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
    1.19        |> Theory.add_path (space_implode "_" new_type_names)
    1.20        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.21 -           weak_case_congs Simplifier.cong_add_global
    1.22 +           weak_case_congs (Attrib.theory Simplifier.cong_add)
    1.23        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.24        |> add_cases_induct dt_infos induct
    1.25        |> Theory.parent_path
    1.26 @@ -806,7 +806,7 @@
    1.27        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
    1.28        |> Theory.add_path (space_implode "_" new_type_names)
    1.29        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.30 -            weak_case_congs (Simplifier.change_global_ss (op addcongs))
    1.31 +            weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
    1.32        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.33        |> add_cases_induct dt_infos induct
    1.34        |> Theory.parent_path
    1.35 @@ -913,7 +913,7 @@
    1.36      val thy11 = thy10 |>
    1.37        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.38        add_rules simps case_thms size_thms rec_thms inject distinct
    1.39 -                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.40 +                weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |> 
    1.41        put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.42        add_cases_induct dt_infos induction' |>
    1.43        Theory.parent_path |>