# HG changeset patch
# User clasohm
# Date 810393079 -7200
# Node ID 2d1c27d1dac3e11eb933f576b4352642dc14162e
# Parent  79692e8ce183b086d7a3f3731f3445108cfa43dd
added enum2 and list2

diff -r 79692e8ce183 -r 2d1c27d1dac3 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Sep 05 18:52:42 1995 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Sep 06 15:11:19 1995 +0200
@@ -36,10 +36,14 @@
     -> token list -> 'a list * token list
   val enum1: string -> (token list -> 'a * token list)
     -> token list -> 'a list * token list
+  val enum2: string -> (token list -> 'a * token list)
+    -> token list -> 'a list * token list
   val list: (token list -> 'a * token list)
     -> token list -> 'a list * token list
   val list1: (token list -> 'a * token list)
     -> token list -> 'a list * token list
+  val list2: (token list -> 'a * token list)
+    -> token list -> 'a list * token list
   val name: token list -> string * token list
   val sort: token list -> string * token list
   val opt_infix: token list -> string * token list
@@ -146,11 +150,12 @@
 fun repeat1 parse = parse -- repeat parse >> op ::;
 
 fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
+fun enum2 sep parse = parse --$$ sep -- enum1 sep parse >> op ::;
 fun enum sep parse = enum1 sep parse || empty;
 
 val list = enum ",";
 val list1 = enum1 ",";
-
+val list2 = enum2 ","; (*list with at least two elements*)
 
 
 (** theory parsers **)