removed obsolete "{}";
authorwenzelm
Sun, 25 Jun 2000 23:48:09 +0200
changeset 9126 ca8c6793dca5
parent 9125 f85564116be1
child 9127 b1dc56410b63
removed obsolete "{}";
src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Jun 25 23:47:47 2000 +0200
+++ b/src/Pure/Isar/args.ML	Sun Jun 25 23:48:09 2000 +0200
@@ -168,7 +168,7 @@
 
 (* args *)
 
-val exclude = explode "(){}[],";
+val exclude = explode "()[],";
 
 fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");