# HG changeset patch
# User blanchet
# Date 1304496764 -7200
# Node ID af86324707f2572a47c9334efd7111ca180d02e3
# Parent  43766deefc16ae0db5e05261aaa10a4db3f9e84e
eta-expansion for SML/NJ

diff -r 43766deefc16 -r af86324707f2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 23:01:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 10:12:44 2011 +0200
@@ -226,12 +226,12 @@
 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
   | combterm_vars (CombConst _) = I
   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
-val close_combformula_universally = close_universally combterm_vars
+fun close_combformula_universally phi = close_universally combterm_vars phi
 
 fun term_vars (ATerm (name as (s, _), tms)) =
   is_atp_variable s ? insert (op =) (name, NONE)
   #> fold term_vars tms
-val close_formula_universally = close_universally term_vars
+fun close_formula_universally phi = close_universally term_vars phi
 
 fun fo_term_from_typ (Type (s, Ts)) =
     ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
@@ -283,7 +283,7 @@
     (hd ss, map unmangled_type (tl ss))
   end
 
-val introduce_proxies =
+fun introduce_proxies tm =
   let
     fun aux top_level (CombApp (tm1, tm2)) =
         CombApp (aux top_level tm1, aux false tm2)
@@ -300,7 +300,7 @@
           | NONE => (name, T_args))
         |> (fn (name, T_args) => CombConst (name, T, T_args))
       | aux _ tm = tm
-  in aux true end
+  in aux true tm end
 
 fun combformula_from_prop thy eq_as_iff =
   let
@@ -474,8 +474,8 @@
         #> fold (aux false) args
       end
   in aux true end
-val add_fact_syms_to_table =
-  fact_lift o formula_fold o add_combterm_syms_to_table
+fun add_fact_syms_to_table explicit_apply =
+  fact_lift (formula_fold (add_combterm_syms_to_table explicit_apply))
 
 val default_sym_table_entries =
   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
@@ -567,7 +567,8 @@
   introduce_explicit_apps_in_combterm sym_tab
   #> introduce_predicators_in_combterm sym_tab
   #> impose_type_arg_policy_in_combterm type_sys
-val repair_fact = update_combformula o formula_map oo repair_combterm
+fun repair_fact type_sys sym_tab =
+  update_combformula (formula_map (repair_combterm type_sys sym_tab))
 
 (** Helper facts **)