1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -693,10 +693,10 @@
     1.4  fun lift_lams_part_1 ctxt type_enc =
     1.5    map (Envir.eta_contract #> close_form) #> rpair ctxt
     1.6    #-> Lambda_Lifting.lift_lambdas
     1.7 -          (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
     1.8 -                   lam_lifted_poly_prefix
     1.9 -                 else
    1.10 -                   lam_lifted_mono_prefix))
    1.11 +          (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
    1.12 +                    lam_lifted_poly_prefix
    1.13 +                  else
    1.14 +                    lam_lifted_mono_prefix) ^ "_a"))
    1.15            Lambda_Lifting.is_quantifier
    1.16    #> fst
    1.17  val lift_lams_part_2 = pairself (map (open_form o constify_lifted))