# HG changeset patch
# User blanchet
# Date 1311595812 -7200
# Node ID 91294d386539ca368f4caa19a02f677c0c4bae1f
# Parent  c2554cc82d34a9515e2d2ed749c6feef6bca0c77
avoid needless type args for lifted-lambdas

diff -r c2554cc82d34 -r 91294d386539 src/HOL/Tools/ATP/atp_translate.ML
--- 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''
diff -r c2554cc82d34 -r 91294d386539 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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