# HG changeset patch
# User clasohm
# Date 810394031 -7200
# Node ID 000ecb4fc700fa5f7713a2fa5975b5b106dfd0f9
# Parent  2d1c27d1dac3e11eb933f576b4352642dc14162e
removed list2 and enum2

diff -r 2d1c27d1dac3 -r 000ecb4fc700 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Sep 06 15:11:19 1995 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Sep 06 15:27:11 1995 +0200
@@ -36,14 +36,10 @@
     -> 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
@@ -150,12 +146,10 @@
 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 **)