--- a/src/HOL/Tools/Qelim/cooper_data.ML Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Thu Mar 26 14:14:02 2009 +0100
@@ -67,6 +67,7 @@
(* concrete syntax *)
local
+
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val constsN = "consts";
@@ -77,14 +78,17 @@
fun optional scan = Scan.optional scan [];
in
-val attribute =
- (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add
+
+val presburger_setup =
+ Attrib.setup @{binding presburger}
+ ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add) "Cooper data";
+
end;
(* theory setup *)
-val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
+val setup = presburger_setup;
end;