diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp
index 7a0bc3d69..a1b9012ed 100644
--- a/src/frontend/parser.cpp
+++ b/src/frontend/parser.cpp
@@ -40,7 +40,7 @@ struct parser_fn {
     typedef std::unordered_map<name, expr, name_hash, name_eq>  builtins;
     frontend       m_frontend;
     scanner        m_scanner;
-    std::ostream & m_err;
+    std::ostream * m_err;
     scanner::token m_curr;
     bool           m_use_exceptions;
     bool           m_found_errors;
@@ -84,7 +84,7 @@ struct parser_fn {
         m_builtins["Int"]    = Int;
     }
 
-    parser_fn(frontend & fe, std::istream & in, std::ostream & err, bool use_exceptions):
+    parser_fn(frontend & fe, std::istream & in, std::ostream * err, bool use_exceptions):
         m_frontend(fe),
         m_scanner(in),
         m_err(err),
@@ -369,7 +369,8 @@ struct parser_fn {
     }
 
     void error(char const * msg, unsigned line, unsigned pos) {
-        m_err << "Error (line: " << line << ", pos: " << pos << ") " << msg << std::endl;
+        lean_assert(m_err);
+        (*m_err) << "Error (line: " << line << ", pos: " << pos << ") " << msg << std::endl;
     }
 
     void error(char const * msg) {
@@ -403,8 +404,20 @@ struct parser_fn {
             }
         }
     }
+
+    expr parse_expr_main() {
+        try {
+            return parse_expr();
+        } catch (parser_error & ex) {
+            throw parser_exception(ex.what(), m_scanner.get_line(), m_scanner.get_pos());
+        }
+    }
+
 };
 bool parse_commands(frontend & fe, std::istream & in, std::ostream & err, bool use_exceptions) {
-    return parser_fn(fe, in, err, use_exceptions).parse_commands();
+    return parser_fn(fe, in, &err, use_exceptions).parse_commands();
+}
+expr parse_expr(frontend const & fe, std::istream & in) {
+    return parser_fn(const_cast<frontend&>(fe), in, nullptr, true).parse_expr_main();
 }
 }
diff --git a/src/frontend/parser.h b/src/frontend/parser.h
index 7a7d713e6..f50016f1d 100644
--- a/src/frontend/parser.h
+++ b/src/frontend/parser.h
@@ -10,4 +10,5 @@ Author: Leonardo de Moura
 
 namespace lean {
 bool parse_commands(frontend & fe, std::istream & in, std::ostream & err = std::cerr, bool use_exceptions = false);
+expr parse_expr(frontend const & fe, std::istream & in);
 }
diff --git a/src/tests/frontend/parser.cpp b/src/tests/frontend/parser.cpp
index a4557c5cb..02d7ea615 100644
--- a/src/tests/frontend/parser.cpp
+++ b/src/tests/frontend/parser.cpp
@@ -5,15 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <sstream>
+#include "builtin.h"
 #include "parser.h"
 #include "pp.h"
 #include "printer.h"
+#include "exception.h"
 #include "test.h"
 using namespace lean;
 
-static void parse(frontend & fe, char const * msg) {
+static void parse(frontend & fe, char const * str) {
     frontend child = fe.mk_child();
-    std::istringstream in(msg);
+    std::istringstream in(str);
     if (parse_commands(child, in)) {
         formatter fmt = mk_pp_formatter(child);
         std::for_each(child.begin_local_objects(),
@@ -27,11 +29,37 @@ static void parse(frontend & fe, char const * msg) {
 
 static void tst1() {
     frontend fe;
-    parse(fe,
-"Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
+    parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
+}
+
+static void check(frontend const & fe, char const * str, expr const & expected) {
+    std::istringstream in(str);
+    try {
+        expr got = parse_expr(fe, in);
+        lean_assert(expected == got);
+    } catch (exception &) {
+        lean_unreachable();
+    }
+}
+
+static void tst2() {
+    frontend fe;
+    fe.add_var("x", Bool);
+    fe.add_var("y", Bool);
+    fe.add_var("z", Bool);
+    expr x = Const("x"); expr y = Const("y"); expr z = Const("z");
+    check(fe, "x && y", And(x, y));
+    check(fe, "x && y || z", Or(And(x, y), z));
+    check(fe, "x || y && z", Or(x, And(y, z)));
+    check(fe, "x || y || x && z", Or(x, Or(y, And(x, z))));
+    check(fe, "x || y || x && z => x && y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
+    check(fe, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
+    check(fe, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x))));
+    check(fe, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x))));
 }
 
 int main() {
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }