# HG changeset patch
# User chaieb
# Date 1084958694 -7200
# Node ID c90bed2d5bdf371e77c9e3bd9a275a69eb7f414d
# Parent  af3b71a46a1cf4ca8277bc07c271986177a0681e
the function list1 has been exported.

diff -r af3b71a46a1c -r c90bed2d5bdf src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed May 19 11:23:59 2004 +0200
+++ b/src/Pure/Isar/args.ML	Wed May 19 11:24:54 2004 +0200
@@ -57,6 +57,8 @@
   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 =