--- a/src/HOL/Tools/Presburger/cooper_data.ML Tue Jun 12 10:15:48 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_data.ML Tue Jun 12 10:15:52 2007 +0200
@@ -64,7 +64,7 @@
(ss delsimps [th], Library.subtract (op aconv) ts' ts )))
(* concrete syntax *)
-
+local
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val constsN = "consts";
@@ -74,10 +74,11 @@
fun optional scan = Scan.optional scan [];
-
+in
fun att_syntax src = src |> Attrib.syntax
((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add);
+ optional (keyword constsN |-- terms) >> add)
+end;
(* theory setup *)