src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
changeset 38652 e063be321438
parent 38618 5536897d04c2
child 38678 1bf1e21d3136
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -119,8 +119,12 @@
             @{const Not} $ t1 => @{const Not} $ aux Ts t1
           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
             t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name All}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
             t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
@@ -175,8 +179,10 @@
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
+              |> transform_elim_term
               |> atomize_term
-    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+    val need_trueprop = (fastype_of t = HOLogic.boolT)
+    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
               |> extensionalize_term
               |> presimp ? presimplify_term thy
               |> perhaps (try (HOLogic.dest_Trueprop))