1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -63,6 +63,7 @@
     1.4    val concealedN : string
     1.5    val liftingN : string
     1.6    val combinatorsN : string
     1.7 +  val hybridN : string
     1.8    val lambdasN : string
     1.9    val smartN : string
    1.10    val dest_dir : string Config.T
    1.11 @@ -337,6 +338,7 @@
    1.12  val concealedN = "concealed"
    1.13  val liftingN = "lifting"
    1.14  val combinatorsN = "combinators"
    1.15 +val hybridN = "hybrid"
    1.16  val lambdasN = "lambdas"
    1.17  val smartN = "smart"
    1.18  
    1.19 @@ -535,6 +537,19 @@
    1.20            Lambda_Lifting.is_quantifier
    1.21    #> fst
    1.22  
    1.23 +fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) =
    1.24 +    intentionalize_def t
    1.25 +  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    1.26 +    let
    1.27 +      fun lam T t = Abs (Name.uu, T, t)
    1.28 +      val (head, args) = strip_comb t ||> rev
    1.29 +      val head_T = fastype_of head
    1.30 +      val n = length args
    1.31 +      val arg_Ts = head_T |> binder_types |> take n |> rev
    1.32 +      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
    1.33 +    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
    1.34 +  | intentionalize_def t = t
    1.35 +
    1.36  fun translate_atp_lambdas ctxt type_enc =
    1.37    Config.get ctxt atp_lambda_translation
    1.38    |> (fn trans =>
    1.39 @@ -553,6 +568,10 @@
    1.40             lift_lambdas ctxt type_enc
    1.41           else if trans = combinatorsN then
    1.42             map (introduce_combinators ctxt) #> rpair []
    1.43 +         else if trans = hybridN then
    1.44 +           lift_lambdas ctxt type_enc
    1.45 +           ##> maps (fn t => [t, introduce_combinators ctxt
    1.46 +                                     (intentionalize_def t)])
    1.47           else if trans = lambdasN then
    1.48             map (Envir.eta_contract) #> rpair []
    1.49           else