src/HOL/Tools/lin_arith.ML

     addSolver (mk_solver' "lin_arith"
       (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   Context.mapping
    (setup_options #>
     Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
-    Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
-      "declaration of split rules for arithmetic procedure")]) I;
+    Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
+      "declaration of split rules for arithmetic procedure") I;
 
 end;
 
 structure BasicLinArith: BASIC_LIN_ARITH = LinArith;
 open BasicLinArith;