src/HOL/Tools/datatype_package.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18751 38dc4ff2a32b
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4         induction : thm,
     1.5         size : thm list,
     1.6         simps : thm list} * theory
     1.7 -  val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
     1.8 -    (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
     1.9 +  val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
    1.10 +    (thm list * attribute list) list list -> (thm list * attribute list) ->
    1.11      theory ->
    1.12        {distinct : thm list list,
    1.13         inject : thm list list,
    1.14 @@ -350,10 +350,10 @@
    1.15                    weak_case_congs cong_att =
    1.16    (snd o PureThy.add_thmss [(("simps", simps), []),
    1.17      (("", List.concat case_thms @ size_thms @ 
    1.18 -          List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
    1.19 +          List.concat distinct  @ rec_thms), [Simplifier.simp_add]),
    1.20      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    1.21 -    (("", List.concat inject),               [Attrib.theory iff_add]),
    1.22 -    (("", map name_notE (List.concat distinct)),  [Attrib.theory (Classical.safe_elim NONE)]),
    1.23 +    (("", List.concat inject),               [iff_add]),
    1.24 +    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim NONE]),
    1.25      (("", weak_case_congs),                  [cong_att])]);
    1.26  
    1.27  
    1.28 @@ -365,10 +365,10 @@
    1.29      fun proj i = ProjectRule.project induction (i + 1);
    1.30  
    1.31      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    1.32 -      [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]),
    1.33 -       (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])];
    1.34 +      [(("", proj index), [InductAttrib.induct_type name]),
    1.35 +       (("", exhaustion), [InductAttrib.cases_type name])];
    1.36      fun unnamed_rule i =
    1.37 -      (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]);
    1.38 +      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
    1.39    in
    1.40      PureThy.add_thms
    1.41        (List.concat (map named_rules infos) @
    1.42 @@ -747,7 +747,7 @@
    1.43        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
    1.44        |> Theory.add_path (space_implode "_" new_type_names)
    1.45        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.46 -           weak_case_congs (Attrib.theory Simplifier.cong_add)
    1.47 +          weak_case_congs Simplifier.cong_add
    1.48        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.49        |> add_cases_induct dt_infos induct
    1.50        |> Theory.parent_path
    1.51 @@ -806,7 +806,7 @@
    1.52        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
    1.53        |> Theory.add_path (space_implode "_" new_type_names)
    1.54        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.55 -            weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
    1.56 +          weak_case_congs (Simplifier.attrib (op addcongs))
    1.57        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.58        |> add_cases_induct dt_infos induct
    1.59        |> Theory.parent_path
    1.60 @@ -913,7 +913,7 @@
    1.61      val thy11 = thy10 |>
    1.62        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.63        add_rules simps case_thms size_thms rec_thms inject distinct
    1.64 -                weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |> 
    1.65 +        weak_case_congs (Simplifier.attrib (op addcongs)) |> 
    1.66        put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.67        add_cases_induct dt_infos induction' |>
    1.68        Theory.parent_path |>