Eta-expanded some declarations that are illegal under value polymorphism
authorpaulson
Wed, 27 Nov 1996 10:40:45 +0100
changeset 2238 c72a23bbe762
parent 2237 f01ac387e82b
child 2239 8f9007a2f165
Eta-expanded some declarations that are illegal under value polymorphism
src/HOL/typedef.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/domain/library.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 []
--- 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);
 
--- 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;