diff --git a/src/main/scala/leon/solvers/isabelle/Translator.scala b/src/main/scala/leon/solvers/isabelle/Translator.scala
index 47d62bb5c7a9677b96e2ebda534794e1e89cc8c0..c0c9446f169e74aba27d19876e23d66915fbfd75 100644
--- a/src/main/scala/leon/solvers/isabelle/Translator.scala
+++ b/src/main/scala/leon/solvers/isabelle/Translator.scala
@@ -44,15 +44,15 @@ final class Translator(context: LeonContext, program: Program, types: Types, sys
   }
 
   def term(expr: Expr, bounds: List[Identifier], consts: (FunDef, Typ) => Term): Future[Term] = {
-    def mkAbs(params: List[Identifier], body: Expr, bounds: List[Identifier]): Future[Term] = params match {
+    def mkAbs(params: List[Identifier], body: Expr, bounds: List[Identifier], wrap: Term => Term = identity): Future[Term] = params match {
       case Nil => term(body, bounds, consts)
       case p :: ps =>
         for {
-          rec <- mkAbs(ps, body, p :: bounds)
+          rec <- mkAbs(ps, body, p :: bounds, wrap)
           typ <- types.typ(p.getType)
         }
         yield
-          Abs(p.mangledName /* name hint, no logical content */, typ, rec)
+          wrap(Abs(p.mangledName /* name hint, no logical content */, typ, rec))
     }
 
     def nary(const: Term, xs: Expr*) =
@@ -180,6 +180,9 @@ final class Translator(context: LeonContext, program: Program, types: Types, sys
       case Lambda(args, expr) =>
         mkAbs(args.map(_.id).toList, expr, bounds)
 
+      case Forall(args, expr) =>
+        mkAbs(args.map(_.id).toList, expr, bounds, wrap = mkApp(Const("HOL.All", Typ.dummyT), _))
+
       case CaseClass(typ, exprs) =>
         lookupConstructor(typ).map(_.term).flatMap { nary(_, exprs: _*) }
 
diff --git a/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala b/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b0e815c576ffd29db1f402a06da66f8046cbfe85
--- /dev/null
+++ b/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object Quantifiers {
+
+  def swapping[A, B](p: (A, B) => Boolean) = {
+    require(forall((x: A, y: B) => p(x, y)))
+    forall((y: B, x: A) => p(x, y))
+  }.holds
+
+  def swapping_curry[A, B](p: A => B => Boolean) = {
+    require(forall((x: A) => forall((y: B) => p(x)(y))))
+    forall((y: B) => forall((x: A) => p(x)(y)))
+  }.holds
+
+  def inst[A](p: A => Boolean, a: A) = {
+    require(forall((x: A) => p(a)))
+    p(a)
+  }.holds
+
+  def exists[A](p: A => Boolean) =
+    !forall((x: A) => !p(x))
+
+  def drinkersPrinciple[A](d: A => Boolean) =
+    exists((x: A) => d(x) ==> forall((y: A) => d(y))).holds
+
+}