src/HOL/Tools/ATP/atp_translate.ML

     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
-  val conceal_lambdas : Proof.context -> term -> term
   val introduce_combinators : Proof.context -> term -> term
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
     -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
     -> term -> ((string * locality) * term) list

 val prefixed_app_op_name = const_prefix ^ app_op_name
 val prefixed_type_tag_name = const_prefix ^ type_tag_name
 
 (* Freshness almost guaranteed! *)
 val atp_weak_prefix = "ATP:"
-
-val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
 
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
   The character _ goes to __
   Characters in the range ASCII space to / go to _A to _P, respectively.

 
 fun do_conceal_lambdas Ts (t1 $ t2) =
     do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
   | do_conceal_lambdas Ts (Abs (_, T, t)) =
     (* slightly unsound because of hash collisions *)
-    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
-          T --> fastype_of1 (Ts, t))
+    Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t))
   | do_conceal_lambdas _ t = t
-val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
 
 fun do_introduce_combinators ctxt Ts t =
   let val thy = Proof_Context.theory_of ctxt in
     t |> conceal_bounds Ts
       |> cterm_of thy