src/ZF/Tools/datatype_package.ML
changeset 18728 6790126ab5f6
parent 18690 16a64bdc5485
child 20046 9c8909fc5865
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 21 23:02:14 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), [Attrib.theory Simplifier.simp_add]),
     1.8 -          (("", intrs), [Attrib.theory (Classical.safe_intro NONE)]),
     1.9 +         [(("simps", simps), [Simplifier.simp_add]),
    1.10 +          (("", intrs), [Classical.safe_intro NONE]),
    1.11            (("con_defs", con_defs), []),
    1.12            (("case_eqns", case_eqns), []),
    1.13            (("recursor_eqns", recursor_eqns), []),