src/Pure/Thy/thy_parse.ML
changeset 2231 71385461570a
parent 2203 c2dbdc2ef781
child 2253 95b615550b8b
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Nov 26 16:29:30 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Nov 26 16:33:59 1996 +0100
     1.3 @@ -149,8 +149,8 @@
     1.4  fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
     1.5  fun enum sep parse = enum1 sep parse || empty;
     1.6  
     1.7 -val list = enum ",";
     1.8 -val list1 = enum1 ",";
     1.9 +fun list  parse = enum  "," parse;
    1.10 +fun list1 parse = enum1 "," parse;
    1.11  
    1.12  
    1.13  (** theory parsers **)
    1.14 @@ -170,7 +170,7 @@
    1.15  fun mk_triple1 ((x, y), z) = mk_triple (x, y, z);
    1.16  fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
    1.17  
    1.18 -val split_decls = flat o map (fn (xs, y) => map (rpair y) xs);
    1.19 +fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
    1.20  
    1.21  fun strip_quotes str =
    1.22    implode (tl (take (size str - 1, explode str)));