# HG changeset patch
# User wenzelm
# Date 961969689 -7200
# Node ID ca8c6793dca594489396cffadf322acba26f8117
# Parent  f85564116be10376cb326038eaf55c82aa6b4186
removed obsolete "{}";

diff -r f85564116be1 -r ca8c6793dca5 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 = ",");