# 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 **)