# 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;