Eta-expansion of a function definition, for value polymorphism

--- a/src/Pure/sign.ML	Tue Nov 26 16:15:50 1996 +0100
+++ b/src/Pure/sign.ML	Tue Nov 26 16:18:42 1996 +0100
@@ -151,7 +151,7 @@
 
 (** print signature **)
 
-val stamp_names = rev o map !;
+fun stamp_names stamps = rev (map ! stamps);
 
 fun print_sg sg =
   let
@@ -424,8 +424,8 @@
     (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   end;
 
-val ext_tyabbrs_i = ext_abbrs (K (K I));
-val ext_tyabbrs = ext_abbrs read_abbr;
+fun ext_tyabbrs_i arg = ext_abbrs (K (K I)) arg;
+fun ext_tyabbrs   arg = ext_abbrs read_abbr arg;
 
 
 (* add type arities *)

--- a/src/Pure/symtab.ML	Tue Nov 26 16:15:50 1996 +0100
+++ b/src/Pure/symtab.ML	Tue Nov 26 16:18:42 1996 +0100
@@ -136,7 +136,7 @@
 fun extend eq (tab, alst) =
   generic_extend (eq_pair eq) dest make tab alst;
 
-val extend_new = extend (K false);
+fun extend_new (tab, alst) = extend (K false) (tab, alst);
 
 fun merge eq (tab1, tab2) =
   generic_merge (eq_pair eq) dest make tab1 tab2;

--- a/src/Pure/tactic.ML	Tue Nov 26 16:15:50 1996 +0100
+++ b/src/Pure/tactic.ML	Tue Nov 26 16:18:42 1996 +0100
@@ -352,7 +352,7 @@
       else    x :: untaglist rest;
 
 (*return list elements in original order*)
-val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
+fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
 
 (*insert one tagged brl into the pair of nets*)
 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =