1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 16:15:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 23:47:27 2011 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val const_prefix : string
     1.5    val type_const_prefix : string
     1.6    val class_prefix : string
     1.7 +  val polymorphic_free_prefix : string
     1.8    val skolem_const_prefix : string
     1.9    val old_skolem_const_prefix : string
    1.10    val new_skolem_const_prefix : string
    1.11 @@ -125,8 +126,7 @@
    1.12  val type_const_prefix = "tc_"
    1.13  val class_prefix = "cl_"
    1.14  
    1.15 -(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *)
    1.16 -val lambda_lifted_prefix = Name.uu
    1.17 +val polymorphic_free_prefix = "poly_free"
    1.18  
    1.19  val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
    1.20  val old_skolem_const_prefix = skolem_const_prefix ^ "o"
    1.21 @@ -480,7 +480,7 @@
    1.22       atyps_of T)
    1.23    | iterm_from_term _ _ (Free (s, T)) =
    1.24      (IConst (`make_fixed_var s, T,
    1.25 -             if String.isPrefix lambda_lifted_prefix s then [T] else []),
    1.26 +             if String.isPrefix polymorphic_free_prefix s then [T] else []),
    1.27       atyps_of T)
    1.28    | iterm_from_term _ _ (Var (v as (s, _), T)) =
    1.29      (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
    1.30 @@ -1417,7 +1417,7 @@
    1.31          if String.isPrefix skolem_const_prefix s then I
    1.32          else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
    1.33        | add (Free (s, T)) =
    1.34 -        if String.isPrefix lambda_lifted_prefix s then
    1.35 +        if String.isPrefix polymorphic_free_prefix s then
    1.36            T |> fold_type_constrs set_insert
    1.37          else
    1.38            I