# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 2231a151db59f456d5a2a156c79545c8b89a5459
# Parent  94ebb64b0433e72b6868dbdd746ce40c7b72cca6
protect prefix against variant mutations

diff -r 94ebb64b0433 -r 2231a151db59 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -693,10 +693,10 @@
 fun lift_lams_part_1 ctxt type_enc =
   map (Envir.eta_contract #> close_form) #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
-          (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
-                   lam_lifted_poly_prefix
-                 else
-                   lam_lifted_mono_prefix))
+          (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
+                    lam_lifted_poly_prefix
+                  else
+                    lam_lifted_mono_prefix) ^ "_a"))
           Lambda_Lifting.is_quantifier
   #> fst
 val lift_lams_part_2 = pairself (map (open_form o constify_lifted))