src/ZF/Tools/datatype_package.ML
changeset 18688 abf0f018b5ec
parent 18418 bf448d999b7e
child 18690 16a64bdc5485
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -367,8 +367,8 @@
     1.4    (*Updating theory components: simprules and datatype info*)
     1.5    (thy1 |> Theory.add_path big_rec_base_name
     1.6          |> PureThy.add_thmss
     1.7 -         [(("simps", simps), [Simplifier.simp_add_global]),
     1.8 -          (("", intrs), [Classical.safe_intro_global]),
     1.9 +         [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
    1.10 +          (("", intrs), [Attrib.theory Classical.safe_intro]),
    1.11            (("con_defs", con_defs), []),
    1.12            (("case_eqns", case_eqns), []),
    1.13            (("recursor_eqns", recursor_eqns), []),