--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 11:21:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 14:10:12 2011 +0200
@@ -1258,7 +1258,8 @@
fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
| aux arity (IConst (name as (s, _), T, T_args)) =
(case strip_prefix_and_unascii const_prefix s of
- NONE => (name, T_args)
+ NONE =>
+ (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
| SOME s'' =>
let
val s'' = invert_const s''
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 11:21:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 25 14:10:12 2011 +0200
@@ -525,10 +525,14 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt =
+fun lift_lambdas ctxt type_enc =
map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
- Lambda_Lifting.is_quantifier
+ #-> Lambda_Lifting.lift_lambdas
+ (if polymorphism_of_type_enc type_enc = Polymorphic then
+ SOME polymorphic_free_prefix
+ else
+ NONE)
+ Lambda_Lifting.is_quantifier
#> fst
fun translate_atp_lambdas ctxt type_enc =
@@ -544,9 +548,9 @@
trans)
|> (fn trans =>
if trans = concealedN then
- lift_lambdas ctxt ##> K []
+ lift_lambdas ctxt type_enc ##> K []
else if trans = liftingN then
- lift_lambdas ctxt
+ lift_lambdas ctxt type_enc
else if trans = combinatorsN then
map (introduce_combinators ctxt) #> rpair []
else if trans = lambdasN then