--- a/src/HOL/Tools/Qelim/cooper_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -77,15 +77,14 @@
fun optional scan = Scan.optional scan [];
in
-val att_syntax = Attrib.syntax
- ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add)
+val attribute =
+ (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add
end;
(* theory setup *)
-val setup =
- Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
+val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
end;