# HG changeset patch
# User blanchet
# Date 1311198447 -7200
# Node ID 127749bbc6390bc7cf65a344464ed251766c38da
# Parent  aa04d1e1e2cc2999894b63e5442c4c283ea88849
use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned

diff -r aa04d1e1e2cc -r 127749bbc639 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 16:15:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 23:47:27 2011 +0200
@@ -39,6 +39,7 @@
   val const_prefix : string
   val type_const_prefix : string
   val class_prefix : string
+  val polymorphic_free_prefix : string
   val skolem_const_prefix : string
   val old_skolem_const_prefix : string
   val new_skolem_const_prefix : string
@@ -125,8 +126,7 @@
 val type_const_prefix = "tc_"
 val class_prefix = "cl_"
 
-(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *)
-val lambda_lifted_prefix = Name.uu
+val polymorphic_free_prefix = "poly_free"
 
 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
@@ -480,7 +480,7 @@
      atyps_of T)
   | iterm_from_term _ _ (Free (s, T)) =
     (IConst (`make_fixed_var s, T,
-             if String.isPrefix lambda_lifted_prefix s then [T] else []),
+             if String.isPrefix polymorphic_free_prefix s then [T] else []),
      atyps_of T)
   | iterm_from_term _ _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
@@ -1417,7 +1417,7 @@
         if String.isPrefix skolem_const_prefix s then I
         else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
       | add (Free (s, T)) =
-        if String.isPrefix lambda_lifted_prefix s then
+        if String.isPrefix polymorphic_free_prefix s then
           T |> fold_type_constrs set_insert
         else
           I
diff -r aa04d1e1e2cc -r 127749bbc639 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 20 16:15:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 20 23:47:27 2011 +0200
@@ -541,7 +541,8 @@
            rpair [] o map (conceal_lambdas ctxt)
          else if trans = liftingN then
            map (close_form o Envir.eta_contract) #> rpair ctxt
-           #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier
+           #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
+                                           Lambda_Lifting.is_quantifier
            #> fst
          else if trans = combinatorsN then
            rpair [] o map (introduce_combinators ctxt)