use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
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
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 16:15:33 2011 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 23:47:27 2011 +0200
2.3 @@ -541,7 +541,8 @@
2.4 rpair [] o map (conceal_lambdas ctxt)
2.5 else if trans = liftingN then
2.6 map (close_form o Envir.eta_contract) #> rpair ctxt
2.7 - #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier
2.8 + #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
2.9 + Lambda_Lifting.is_quantifier
2.10 #> fst
2.11 else if trans = combinatorsN then
2.12 rpair [] o map (introduce_combinators ctxt)