src/Pure/Thy/thy_parse.ML
changeset 1250 000ecb4fc700
parent 1249 2d1c27d1dac3
child 1321 9a6e7bd2bfaf
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Sep 06 15:11:19 1995 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Sep 06 15:27:11 1995 +0200
     1.3 @@ -36,14 +36,10 @@
     1.4      -> token list -> 'a list * token list
     1.5    val enum1: string -> (token list -> 'a * token list)
     1.6      -> token list -> 'a list * token list
     1.7 -  val enum2: string -> (token list -> 'a * token list)
     1.8 -    -> token list -> 'a list * token list
     1.9    val list: (token list -> 'a * token list)
    1.10      -> token list -> 'a list * token list
    1.11    val list1: (token list -> 'a * token list)
    1.12      -> token list -> 'a list * token list
    1.13 -  val list2: (token list -> 'a * token list)
    1.14 -    -> token list -> 'a list * token list
    1.15    val name: token list -> string * token list
    1.16    val sort: token list -> string * token list
    1.17    val opt_infix: token list -> string * token list
    1.18 @@ -150,12 +146,10 @@
    1.19  fun repeat1 parse = parse -- repeat parse >> op ::;
    1.20  
    1.21  fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
    1.22 -fun enum2 sep parse = parse --$$ sep -- enum1 sep parse >> op ::;
    1.23  fun enum sep parse = enum1 sep parse || empty;
    1.24  
    1.25  val list = enum ",";
    1.26  val list1 = enum1 ",";
    1.27 -val list2 = enum2 ","; (*list with at least two elements*)
    1.28  
    1.29  
    1.30  (** theory parsers **)