src/HOL/Tools/ATP/atp_util.ML

   val s_not : term -> term
   val s_conj : term * term -> term
   val s_disj : term * term -> term
   val s_imp : term * term -> term
   val s_iff : term * term -> term
+  val close_form_prefix : string
   val close_form : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term

   | s_imp p = HOLogic.mk_imp p
 fun s_iff (@{const True}, t2) = t2
   | s_iff (t1, @{const True}) = t1
   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
+val close_form_prefix = "ATP.close_form."
+
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
            HOLogic.all_const T
-           $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
+           $ Abs (close_form_prefix ^ s, T,
+                  abstract_over (Var ((s, i), T), t')))
        (Term.add_vars t []) t
 
 fun monomorphic_term subst =
   map_types (map_type_tvar (fn v =>
       case Type.lookup subst v of