Eta-expansion of a function definition, for value polymorphism
authorpaulson
Tue Nov 26 16:18:42 1996 +0100 (1996-11-26)
changeset 2228f381c1a98209
parent 2227 18e993700540
child 2229 64acb485ecce
Eta-expansion of a function definition, for value polymorphism
src/Pure/sign.ML
src/Pure/symtab.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/sign.ML	Tue Nov 26 16:15:50 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Nov 26 16:18:42 1996 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5  (** print signature **)
     1.6  
     1.7 -val stamp_names = rev o map !;
     1.8 +fun stamp_names stamps = rev (map ! stamps);
     1.9  
    1.10  fun print_sg sg =
    1.11    let
    1.12 @@ -424,8 +424,8 @@
    1.13      (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
    1.14    end;
    1.15  
    1.16 -val ext_tyabbrs_i = ext_abbrs (K (K I));
    1.17 -val ext_tyabbrs = ext_abbrs read_abbr;
    1.18 +fun ext_tyabbrs_i arg = ext_abbrs (K (K I)) arg;
    1.19 +fun ext_tyabbrs   arg = ext_abbrs read_abbr arg;
    1.20  
    1.21  
    1.22  (* add type arities *)
     2.1 --- a/src/Pure/symtab.ML	Tue Nov 26 16:15:50 1996 +0100
     2.2 +++ b/src/Pure/symtab.ML	Tue Nov 26 16:18:42 1996 +0100
     2.3 @@ -136,7 +136,7 @@
     2.4  fun extend eq (tab, alst) =
     2.5    generic_extend (eq_pair eq) dest make tab alst;
     2.6  
     2.7 -val extend_new = extend (K false);
     2.8 +fun extend_new (tab, alst) = extend (K false) (tab, alst);
     2.9  
    2.10  fun merge eq (tab1, tab2) =
    2.11    generic_merge (eq_pair eq) dest make tab1 tab2;
     3.1 --- a/src/Pure/tactic.ML	Tue Nov 26 16:15:50 1996 +0100
     3.2 +++ b/src/Pure/tactic.ML	Tue Nov 26 16:18:42 1996 +0100
     3.3 @@ -352,7 +352,7 @@
     3.4        else    x :: untaglist rest;
     3.5  
     3.6  (*return list elements in original order*)
     3.7 -val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
     3.8 +fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
     3.9  
    3.10  (*insert one tagged brl into the pair of nets*)
    3.11  fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =