src/HOL/arith_data.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 19043 6c0fca729f33
     1.1 --- a/src/HOL/arith_data.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -223,8 +223,9 @@
     1.4    fun print _ _ = ();
     1.5  end);
     1.6  
     1.7 -fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
     1.8 -  {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
     1.9 +val arith_split_add = Thm.declaration_attribute (fn thm =>
    1.10 +  Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
    1.11 +    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger})));
    1.12  
    1.13  fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
    1.14    {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
    1.15 @@ -584,7 +585,5 @@
    1.16    Method.add_methods
    1.17      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    1.18        "decide linear arithmethic")] #>
    1.19 -  Attrib.add_attributes [("arith_split",
    1.20 -    (Attrib.no_args arith_split_add,
    1.21 -     Attrib.no_args Attrib.undef_local_attribute),
    1.22 +  Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
    1.23      "declaration of split rules for arithmetic procedure")];