# HG changeset patch
# User wenzelm
# Date 924277711 -7200
# Node ID 83d8dabdae9a9427f67bd403e4827cc0e451edff
# Parent  583add9799c37bd51e07fd58e446b3eca6ed63f9
lifted enum;
removed list(1);
added and_list(1);

diff -r 583add9799c3 -r 83d8dabdae9a src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri Apr 16 17:47:06 1999 +0200
+++ b/src/Pure/Isar/args.ML	Fri Apr 16 17:48:31 1999 +0200
@@ -22,10 +22,10 @@
   val name: T list -> string * T list
   val nat: T list -> int * T list
   val var: T list -> indexname * T list
-  val enum1: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
-  val enum: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
-  val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
-  val list: (T list -> 'a * T list) -> T list -> 'a list * T list
+  val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
+  val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
+  val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
+  val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val global_typ: theory * T list -> typ * (theory * T list)
   val global_term: theory * T list -> term * (theory * T list)
   val global_prop: theory * T list -> term * (theory * T list)
@@ -116,11 +116,11 @@
 
 (* enumerations *)
 
-fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
+fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
-fun list1 scan = enum1 "," scan;
-fun list scan = enum "," scan;
+fun and_list1 scan = enum1 "and" scan;
+fun and_list scan = enum "and" scan;
 
 
 (* terms and types *)
@@ -183,6 +183,9 @@
 
 (* attribs *)
 
+fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
+fun list scan = list1 scan || Scan.succeed [];
+
 val attrib = position (name -- !!! (args false)) >> src;
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];