# HG changeset patch # User paulson # Date 849087645 -3600 # Node ID c72a23bbe76218115e2cfc166f2b22f3db1fc15e # Parent f01ac387e82b0f64511583ffa90ef15e117ec587 Eta-expanded some declarations that are illegal under value polymorphism diff -r f01ac387e82b -r c72a23bbe762 src/HOL/typedef.ML --- a/src/HOL/typedef.ML Wed Nov 27 10:36:38 1996 +0100 +++ b/src/HOL/typedef.ML Wed Nov 27 10:40:45 1996 +0100 @@ -80,7 +80,7 @@ (* errors *) - val show_names = commas_quote o map fst; + fun show_names pairs = commas_quote (map fst pairs); val illegal_vars = if null (term_vars set) andalso null (term_tvars set) then [] diff -r f01ac387e82b -r c72a23bbe762 src/HOLCF/ax_ops/thy_ops.ML --- a/src/HOLCF/ax_ops/thy_ops.ML Wed Nov 27 10:36:38 1996 +0100 +++ b/src/HOLCF/ax_ops/thy_ops.ML Wed Nov 27 10:40:45 1996 +0100 @@ -371,7 +371,7 @@ val names1 = list1 name; -val split_decls = flat o map (fn (xs, y) => map (rpair y) xs); +fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls); fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z); diff -r f01ac387e82b -r c72a23bbe762 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Wed Nov 27 10:36:38 1996 +0100 +++ b/src/HOLCF/domain/library.ML Wed Nov 27 10:40:45 1996 +0100 @@ -89,8 +89,8 @@ typ list) * (* arguments of abstracted type *) cons list; (* represented type, as a constructor list *) -val rec_of = snd o first; -val is_lazy = fst o first; +fun rec_of arg = snd (first arg); +fun is_lazy arg = fst (first arg); val sel_of = second; val vname = third; val upd_vname = upd_third;