diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f9c94b5f2..9f3d2e788 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -927,9 +927,9 @@ class parser::imp {
     expr parse_lparen() {
         auto p = pos();
         next();
-        expr r = save(parse_expr(), p);
+        expr r = curr() == scanner::token::Type ? parse_type(true) : parse_expr();
         check_rparen_next("invalid expression, ')' expected");
-        return r;
+        return save(r, p);
     }
 
     /**
@@ -1168,13 +1168,13 @@ class parser::imp {
     }
 
     /** \brief Parse <tt>'Type'</tt> and <tt>'Type' level</tt> expressions. */
-    expr parse_type() {
+    expr parse_type(bool level_expected) {
         auto p = pos();
         next();
-        if (curr_is_identifier() || curr_is_nat()) {
+        if (level_expected) {
             return save(mk_type(parse_level()), p);
         } else {
-            return Type();
+            return save(Type(), p);
         }
     }
 
@@ -1267,7 +1267,7 @@ class parser::imp {
         case scanner::token::DecimalVal:  return parse_decimal();
         case scanner::token::StringVal:   return parse_string();
         case scanner::token::Placeholder: return parse_placeholder();
-        case scanner::token::Type:        return parse_type();
+        case scanner::token::Type:        return parse_type(false);
         case scanner::token::Show:        return parse_show_expr();
         case scanner::token::By:          return parse_by_expr();
         default:
@@ -1279,6 +1279,8 @@ class parser::imp {
        \brief Create a new application and associate position of left with the resultant expression.
     */
     expr mk_app_left(expr const & left, expr const & arg) {
+        if (is_type(left))
+            throw parser_error("Type is not a function, use '(Type <universe>)' for specifying a particular type universe", pos());
         auto it = m_expr_pos_info.find(left);
         lean_assert(it != m_expr_pos_info.end());
         return save(mk_app(left, arg), it->second);
@@ -1297,7 +1299,7 @@ class parser::imp {
         case scanner::token::DecimalVal:  return mk_app_left(left, parse_decimal());
         case scanner::token::StringVal:   return mk_app_left(left, parse_string());
         case scanner::token::Placeholder: return mk_app_left(left, parse_placeholder());
-        case scanner::token::Type:        return mk_app_left(left, parse_type());
+        case scanner::token::Type:        return mk_app_left(left, parse_type(false));
         default:                          return left;
         }
     }
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
index 1756b793f..adb6dd827 100644
--- a/src/tests/frontends/lean/parser.cpp
+++ b/src/tests/frontends/lean/parser.cpp
@@ -86,7 +86,7 @@ static void tst3() {
     parse_error(env, ios, "Help Echo");
     check(env, ios, "10.3", mk_real_value(mpq(103, 10)));
     parse(env, ios, "Variable f : Real -> Real. Check f 10.3.");
-    parse(env, ios, "Variable g : Type 1 -> Type. Check g Type");
+    parse(env, ios, "Variable g : (Type 1) -> Type. Check g Type");
     parse_error(env, ios, "Check fun .");
     parse_error(env, ios, "Definition foo .");
     parse_error(env, ios, "Check a");
diff --git a/tests/lean/conv.lean b/tests/lean/conv.lean
index f96da3a38..9d1f0be6f 100644
--- a/tests/lean/conv.lean
+++ b/tests/lean/conv.lean
@@ -1,18 +1,18 @@
 
 
 
-Definition id (A : Type) : Type U := A.
+Definition id (A : Type) : (Type U) := A.
 Variable p : (Int -> Int) -> Bool.
 Check fun (x : id Int), x.
 Variable f : (id Int) -> (id Int).
 Check p f.
 
-Definition c (A : Type 3) : Type 3 := Type 1.
+Definition c (A : (Type 3)) : (Type 3) := (Type 1).
 Variable g : (c (Type 2)) -> Bool.
 Variable a : (c (Type 1)).
 Check g a.
 
-Definition c2 {T : Type} (A : Type 3) (a : T) : Type 3 := Type 1
+Definition c2 {T : Type} (A : (Type 3)) (a : T) : (Type 3) := (Type 1)
 Variable b : Int
 Check c2::explicit
 Variable g2 : (c2 (Type 2) b) -> Bool
diff --git a/tests/lean/elab6.lean b/tests/lean/elab6.lean
index 7f913193e..be1ea8590 100644
--- a/tests/lean/elab6.lean
+++ b/tests/lean/elab6.lean
@@ -1,2 +1,2 @@
-Theorem ForallIntro2 (A : Type U) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
+Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
         Abst (fun x, EqTIntro (H x))
diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean
index fe2f8f070..7708b9417 100644
--- a/tests/lean/elab7.lean
+++ b/tests/lean/elab7.lean
@@ -1,6 +1,4 @@
-Variable A : Type U
-Variable B : Type U
-Variable C : Type U
+Variables A B C : (Type U)
 Variable P : A -> Bool
 Variable F1 : A -> B -> C
 Variable F2 : A -> B -> C
diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean
index eedecb73a..8db4891c2 100644
--- a/tests/lean/exists3.lean
+++ b/tests/lean/exists3.lean
@@ -16,7 +16,7 @@ Theorem T2 : exists x y, P x y :=
               in ExistsElim L2 (fun (w : Int) (H : P 0 w),
                                     Absurd H (ForallElim (ForallElim L1 0) w))).
 
-Theorem T3 (A : Type U) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
+Theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
     Refute (fun R : not (exists x y, P x y),
               let L1 : forall x y, not (P x y) := ForallIntro (fun a,
                                                      ForallIntro (fun b,
diff --git a/tests/lean/norm1.lean b/tests/lean/norm1.lean
index 28a17f05d..7a434f154 100644
--- a/tests/lean/norm1.lean
+++ b/tests/lean/norm1.lean
@@ -8,7 +8,7 @@ Eval fun f : N -> N, (fun x y : N, g x) (f a)
 Eval fun (a : N) (f : N -> N) (g : (N -> N) -> N -> N) (h : N -> N -> N),
      (fun (x : N) (y : N) (z : N), h x y) (g (fun x : N, f (f x)) (f a)) (f a)
 Eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a == b)
-Eval fun (a : Type) (b : a -> Type) (g : Type U -> Bool), (fun x y : Type U, g x) (Pi x : a, b x)
+Eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (Pi x : a, b x)
 Eval fun f : N -> N, (fun x y z : N, g x) (f a)
 Eval fun f g : N -> N, (fun x y z : N, g x) (f a)
 Eval fun f : N -> N, (fun x : N, fun y : N, fun z : N, P x y z) (f a)
diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean
index bb127385d..805736798 100644
--- a/tests/lean/revapp.lean
+++ b/tests/lean/revapp.lean
@@ -1,4 +1,4 @@
-Definition revapp {A : Type U} {B : A -> Type U} (a : A) (f : Pi (x : A), B x) : (B a) := f a.
+Definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : Pi (x : A), B x) : (B a) := f a.
 Infixl 100 |> : revapp
 
 Eval 10 |> (fun x, x + 1)
@@ -7,7 +7,7 @@ Eval 10 |> (fun x, x + 1)
         |> (fun x, 3 - x)
         |> (fun x, x + 2)
 
-Definition revcomp {A B C: Type U} (f : A -> B) (g : B -> C) : A -> C :=
+Definition revcomp {A B C: (Type U)} (f : A -> B) (g : B -> C) : A -> C :=
         fun x, g (f x)
 Infixl 100 #> : revcomp
 
diff --git a/tests/lean/tactic7.lean b/tests/lean/tactic7.lean
index 6bcfe2228..50334e64f 100644
--- a/tests/lean/tactic7.lean
+++ b/tests/lean/tactic7.lean
@@ -1,25 +1,25 @@
-Variable Eq      {A : Type U+1} (a b : A) : Bool
+Variable Eq      {A : (Type U+1)} (a b : A) : Bool
 Infix 50 === : Eq
-Axiom EqSubst {A : Type U+1} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b
-Axiom EqRefl  {A : Type U+1} (a : A) : a === a
-Theorem EqSymm {A : Type U+1} {a b : A} (H : a === b) : b === a :=
+Axiom EqSubst {A : (Type U+1)} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b
+Axiom EqRefl  {A : (Type U+1)} (a : A) : a === a
+Theorem EqSymm {A : (Type U+1)} {a b : A} (H : a === b) : b === a :=
         EqSubst (fun x, x === a) (EqRefl a) H
-Theorem EqTrans {A : Type U+1} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c :=
+Theorem EqTrans {A : (Type U+1)} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c :=
         EqSubst (fun x, a === x) H1 H2
-Theorem EqCongr {A B : Type U+1} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) :=
+Theorem EqCongr {A B : (Type U+1)} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) :=
         EqSubst (fun x, (f a) === (f x)) (EqRefl (f a)) H
-Theorem EqCongr1 {A : Type U+1} {B : A -> Type U+1} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) :=
+Theorem EqCongr1 {A : (Type U+1)} {B : A -> (Type U+1)} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) :=
         EqSubst (fun h : (Pi x : A, B x), (f a) === (h a)) (EqRefl (f a)) H
 Axiom ProofIrrelevance (P : Bool) (pr1 pr2 : P) : pr1 === pr2
-Axiom EqCast {A B : Type U} (H : A === B) (a : A) : B
-Axiom EqCastHom {A B : Type U} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2)
-Axiom EqCastRefl {A : Type U} (a : A) : (EqCast (EqRefl A) a) === a
+Axiom EqCast {A B : (Type U)} (H : A === B) (a : A) : B
+Axiom EqCastHom {A B : (Type U)} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2)
+Axiom EqCastRefl {A : (Type U)} (a : A) : (EqCast (EqRefl A) a) === a
 
 Variable Vector : (Type U) -> Nat -> (Type U)
-Variable empty {A : Type U} : Vector A 0
-Variable append {A : Type U} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n)
+Variable empty {A : (Type U)} : Vector A 0
+Variable append {A : (Type U)} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n)
 Axiom Plus0 (n : Nat) : (n + 0) === n
-Theorem VectorPlus0 (A : Type U) (n : Nat) : (Vector A (n + 0)) === (Vector A n) :=
+Theorem VectorPlus0 (A : (Type U)) (n : Nat) : (Vector A (n + 0)) === (Vector A n) :=
         EqSubst (fun x : Nat, (Vector A x) === (Vector A n))
                 (EqRefl (Vector A n))
                 (EqSymm (Plus0 n))
@@ -27,8 +27,8 @@ SetOption pp::implicit true
 (* Check fun (A : Type) (n : Nat), VectorPlus0 A n *)
 Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v
 
-Variable List : Type U -> Type U.
-Variables A B : Type U
+Variable List : (Type U) -> (Type U).
+Variables A B : (Type U)
 Axiom H1 : A === B.
 Theorem LAB : (List A) === (List B) :=
         EqCongr List H1
@@ -38,13 +38,13 @@ Variable H2 : (EqCast LAB l1) == l2
 
 
 (*
-Theorem EqCastInv {A B : Type U} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a :=
+Theorem EqCastInv {A B : (Type U)} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a :=
 *)
 
 (*
-Variable ReflCast : Pi (A : Type U) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a
-Theorem AppEq (A : Type U) (B : A -> Type U) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) :=
+Variable ReflCast : Pi (A : (Type U)) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a
+Theorem AppEq (A : (Type U)) (B : A -> (Type U)) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) :=
         EqCongr A (Type U) B b a (EqSymm A a b H)
-Theorem EqCongr2 (A : Type U) (B : A -> Type U) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) :=
+Theorem EqCongr2 (A : (Type U)) (B : A -> (Type U)) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) :=
         EqSubst (B a) a b (fun x : A, Eq (B a) (f a) (Casting (B x) (B a) (AppEq A B a b H) (f a)) (f x)
 *)
\ No newline at end of file
diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean
index 1b2fedc44..5c1256f24 100644
--- a/tests/lean/tst15.lean
+++ b/tests/lean/tst15.lean
@@ -1,20 +1,20 @@
-Variable x : Type max U+1+2 M+1 M+2 3
+Variable x : (Type max U+1+2 M+1 M+2 3)
 Check x
-Variable f : Type U+10 -> Type
+Variable f : (Type U+10) -> Type
 Check f
 Check f x
-Check Type 4
+Check (Type 4)
 Check x
-Check Type max U M
-Show Type U+3
-Check Type U+3
-Check Type U ⊔ M
-Check Type U ⊔ M ⊔ 3
-Show Type U+1 ⊔ M ⊔ 3
-Check Type U+1 ⊔ M ⊔ 3
-Show Type U -> Type 5
-Check Type U -> Type 5
-Check Type M ⊔ 3 -> Type U+5
-Show Type M ⊔ 3 -> Type U -> Type 5
-Check Type M ⊔ 3 -> Type U -> Type 5
-Show Type U
+Check (Type max U M)
+Show (Type U+3)
+Check (Type U+3)
+Check (Type U ⊔ M)
+Check (Type U ⊔ M ⊔ 3)
+Show (Type U+1 ⊔ M ⊔ 3)
+Check (Type U+1 ⊔ M ⊔ 3)
+Show (Type U) -> (Type 5)
+Check (Type U) -> (Type 5)
+Check (Type M ⊔ 3) -> (Type U+5)
+Show (Type M ⊔ 3) -> (Type U) -> (Type 5)
+Check (Type M ⊔ 3) -> (Type U) -> (Type 5)
+Show (Type U)
diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean
index ca3cd1d30..b72d2bfab 100644
--- a/tests/lean/tst7.lean
+++ b/tests/lean/tst7.lean
@@ -3,7 +3,7 @@ Show fun (A B : Type) (a : _), f B a
 (* The following one should produce an error *)
 Show fun (A : Type) (a : _) (B : Type), f B a
 
-Variable myeq : Pi (A : Type U), A -> A -> Bool
+Variable myeq : Pi A : (Type U), A -> A -> Bool
 Show  myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
 Check myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
 
diff --git a/tests/lean/ty2.lean b/tests/lean/ty2.lean
index f07cbfc64..31d897482 100644
--- a/tests/lean/ty2.lean
+++ b/tests/lean/ty2.lean
@@ -1,5 +1,5 @@
-Definition B : Type   := Bool
-Definition T : Type 1 := Type
+Definition B : Type     := Bool
+Definition T : (Type 1) := Type
 Variable N : T
 Variable x : N
 Variable a : B