Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
protect prefix against variant mutations
authorblanchet
Fri, 18 Nov 2011 11:47:12 +0100
changeset 45564 2231a151db59
parent 45563 94ebb64b0433
child 45565 9c335d69a362
protect prefix against variant mutations
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle