src/HOL/Tools/lin_arith.ML
changeset 30528 7173bf123335
parent 30515 bca05b17b618
child 30686 47a32dd1b86e
--- a/src/HOL/Tools/lin_arith.ML	Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 15 15:59:44 2009 +0100
@@ -930,8 +930,8 @@
   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;