1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 21 08:33:57 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 21 21:29:10 2011 +0200
     1.3 @@ -88,7 +88,6 @@
     1.4    val unmangled_const_name : string -> string
     1.5    val helper_table : ((string * bool) * thm list) list
     1.6    val factsN : string
     1.7 -  val conceal_lambdas : Proof.context -> term -> term
     1.8    val introduce_combinators : Proof.context -> term -> term
     1.9    val prepare_atp_problem :
    1.10      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
    1.11 @@ -161,8 +160,6 @@
    1.12  (* Freshness almost guaranteed! *)
    1.13  val atp_weak_prefix = "ATP:"
    1.14  
    1.15 -val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
    1.16 -
    1.17  (*Escaping of special characters.
    1.18    Alphanumeric characters are left unchanged.
    1.19    The character _ goes to __
    1.20 @@ -926,10 +923,8 @@
    1.21      do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
    1.22    | do_conceal_lambdas Ts (Abs (_, T, t)) =
    1.23      (* slightly unsound because of hash collisions *)
    1.24 -    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    1.25 -          T --> fastype_of1 (Ts, t))
    1.26 +    Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t))
    1.27    | do_conceal_lambdas _ t = t
    1.28 -val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
    1.29  
    1.30  fun do_introduce_combinators ctxt Ts t =
    1.31    let val thy = Proof_Context.theory_of ctxt in

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 21 08:33:57 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 21 21:29:10 2011 +0200
     2.3 @@ -525,6 +525,12 @@
     2.4     | NONE => type_enc_from_string best_type_enc)
     2.5    |> choose_format formats
     2.6  
     2.7 +fun lift_lambdas ctxt =
     2.8 +  map (close_form o Envir.eta_contract) #> rpair ctxt
     2.9 +  #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
    2.10 +                                  Lambda_Lifting.is_quantifier
    2.11 +  #> fst
    2.12 +
    2.13  fun translate_atp_lambdas ctxt type_enc =
    2.14    Config.get ctxt atp_lambda_translation
    2.15    |> (fn trans =>
    2.16 @@ -538,16 +544,13 @@
    2.17             trans)
    2.18    |> (fn trans =>
    2.19           if trans = concealedN then
    2.20 -           rpair [] o map (conceal_lambdas ctxt)
    2.21 +           lift_lambdas ctxt ##> K []
    2.22           else if trans = liftingN then
    2.23 -           map (close_form o Envir.eta_contract) #> rpair ctxt
    2.24 -           #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
    2.25 -                                           Lambda_Lifting.is_quantifier
    2.26 -           #> fst
    2.27 +           lift_lambdas ctxt
    2.28           else if trans = combinatorsN then
    2.29 -           rpair [] o map (introduce_combinators ctxt)
    2.30 +           map (introduce_combinators ctxt) #> rpair []
    2.31           else if trans = lambdasN then
    2.32 -           rpair [] o map (Envir.eta_contract)
    2.33 +           map (Envir.eta_contract) #> rpair []
    2.34           else
    2.35             error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    2.36