# HG changeset patch
# User paulson
# Date 849022439 -3600
# Node ID 71385461570a31581adaaf87c06087100fff536a
# Parent  275a5a699ff714d2427e79cf4b1987e2664ac43a
Eta-expansion of a function definition, for value polymorphism

diff -r 275a5a699ff7 -r 71385461570a src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Nov 26 16:29:30 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Nov 26 16:33:59 1996 +0100
@@ -149,8 +149,8 @@
 fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
 fun enum sep parse = enum1 sep parse || empty;
 
-val list = enum ",";
-val list1 = enum1 ",";
+fun list  parse = enum  "," parse;
+fun list1 parse = enum1 "," parse;
 
 
 (** theory parsers **)
@@ -170,7 +170,7 @@
 fun mk_triple1 ((x, y), z) = mk_triple (x, y, z);
 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
 
-val split_decls = flat o map (fn (xs, y) => map (rpair y) xs);
+fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
 
 fun strip_quotes str =
   implode (tl (take (size str - 1, explode str)));