# HG changeset patch
# User paulson
# Date 849021078 -3600
# Node ID f3c6a22681b1399e55c98bb1d5422604eb832347
# Parent  78a8faae780ff037ed7e5cb082e74d916cd1c93d
Eta-expansion of a function definition, for value polymorphism

diff -r 78a8faae780f -r f3c6a22681b1 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Nov 26 16:07:17 1996 +0100
+++ b/src/Pure/display.ML	Tue Nov 26 16:11:18 1996 +0100
@@ -131,7 +131,7 @@
     | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
     | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
 
-  val sort = map (apsnd sort_strings);
+  fun sort l = map (apsnd sort_strings) l;
 in
   fun type_env t = sort (add_type_env (t, []));
   fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
diff -r 78a8faae780f -r f3c6a22681b1 src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Nov 26 16:07:17 1996 +0100
+++ b/src/Pure/net.ML	Tue Nov 26 16:11:18 1996 +0100
@@ -203,7 +203,7 @@
 	     | _ => rands t (net, var::nets)	(*var could match also*)
   end;
 
-val extract_leaves = flat o map (fn Leaf(xs) => xs);
+fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
 
 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
 fun match_term net t = 
diff -r 78a8faae780f -r f3c6a22681b1 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Nov 26 16:07:17 1996 +0100
+++ b/src/ZF/ind_syntax.ML	Tue Nov 26 16:11:18 1996 +0100
@@ -97,7 +97,7 @@
                mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   in  map mk_intr constructs  end;
 
-val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
+fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
 
 val Un          = Const("op Un", [iT,iT]--->iT)
 and empty       = Const("0", iT)