# HG changeset patch
# User blanchet
# Date 1340702080 -7200
# Node ID b3c5c5361e80cd54857c94903b65c4bb9e37b8a0
# Parent  0186df5074c8b3f4ea7d8defd851582750454610
tuning

diff -r 0186df5074c8 -r b3c5c5361e80 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -181,7 +181,7 @@
 val combs_and_liftingN = "combs_and_lifting"
 val combs_or_liftingN = "combs_or_lifting"
 val keep_lamsN = "keep_lams"
-val lam_liftingN = "lam_lifting" (* legacy *)
+val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *)
 
 val bound_var_prefix = "B_"
 val all_bound_var_prefix = "A_"
@@ -1012,8 +1012,6 @@
     not (member (op =) bounds name) ? insert (op =) (name, SOME T)
   | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
 
-fun close_iformula_universally phi = close_universally add_iterm_vars phi
-
 fun aliased_uncurried ary (s, s') =
   (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
 fun unaliased_uncurried (s, s') =
@@ -1279,7 +1277,7 @@
     val (iformula, atomic_Ts) =
       iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
                          []
-      |>> close_iformula_universally
+      |>> close_universally add_iterm_vars
   in
     {name = name, stature = stature, role = role, iformula = iformula,
      atomic_types = atomic_Ts}