# HG changeset patch
# User chaieb
# Date 1181636152 -7200
# Node ID 21a7433c4bd343b459118692bb7d9050ad413fa7
# Parent  42b827dfa86b05a1731978617ecb4675e1e6b736
changed val restriction to local due to smlnj

diff -r 42b827dfa86b -r 21a7433c4bd3 src/HOL/Tools/Presburger/cooper_data.ML
--- 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 *)