# HG changeset patch
# User wenzelm
# Date 1085836256 -7200
# Node ID 72607f591d24ca9a15c7ef109948e78e94e5e549
# Parent  3a1fe2c524d0b12ca593d02583db42400c1eeeaf
do *not* export list/list1 -- commas considered special in arg syntax;

diff -r 3a1fe2c524d0 -r 72607f591d24 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat May 29 15:10:30 2004 +0200
+++ b/src/Pure/Isar/args.ML	Sat May 29 15:10:56 2004 +0200
@@ -57,8 +57,6 @@
   val attribs: T list -> src list * T list
   val opt_attribs: T list -> src list * T list
   val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
-  val list: (T list -> 'a * T list) -> T list -> 'a list * T list
-  val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
 end;
 
 structure Args: ARGS =