removed list2 and enum2
authorclasohm
Wed, 06 Sep 1995 15:27:11 +0200
changeset 1250 000ecb4fc700
parent 1249 2d1c27d1dac3
child 1251 81fc4d8e3eda
removed list2 and enum2
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 **)