Eta-expansion of a function definition, for value polymorphism
authorpaulson
Tue Nov 26 16:11:18 1996 +0100 (1996-11-26)
changeset 2226f3c6a22681b1
parent 2225 78a8faae780f
child 2227 18e993700540
Eta-expansion of a function definition, for value polymorphism
src/Pure/display.ML
src/Pure/net.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/Pure/display.ML	Tue Nov 26 16:07:17 1996 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Nov 26 16:11:18 1996 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4      | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
     1.5      | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
     1.6  
     1.7 -  val sort = map (apsnd sort_strings);
     1.8 +  fun sort l = map (apsnd sort_strings) l;
     1.9  in
    1.10    fun type_env t = sort (add_type_env (t, []));
    1.11    fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
     2.1 --- a/src/Pure/net.ML	Tue Nov 26 16:07:17 1996 +0100
     2.2 +++ b/src/Pure/net.ML	Tue Nov 26 16:11:18 1996 +0100
     2.3 @@ -203,7 +203,7 @@
     2.4  	     | _ => rands t (net, var::nets)	(*var could match also*)
     2.5    end;
     2.6  
     2.7 -val extract_leaves = flat o map (fn Leaf(xs) => xs);
     2.8 +fun extract_leaves l = flat (map (fn Leaf(xs) => xs) l);
     2.9  
    2.10  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
    2.11  fun match_term net t = 
     3.1 --- a/src/ZF/ind_syntax.ML	Tue Nov 26 16:07:17 1996 +0100
     3.2 +++ b/src/ZF/ind_syntax.ML	Tue Nov 26 16:11:18 1996 +0100
     3.3 @@ -97,7 +97,7 @@
     3.4                 mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
     3.5    in  map mk_intr constructs  end;
     3.6  
     3.7 -val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
     3.8 +fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
     3.9  
    3.10  val Un          = Const("op Un", [iT,iT]--->iT)
    3.11  and empty       = Const("0", iT)