# 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)