From b9c62af37dddef5185493fcc6c2ed12a05eaa57e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Aug 2016 11:40:39 -0700
Subject: [PATCH] feat(frontends/lean/parser): remove unnecessary restriction

---
 src/frontends/lean/parser.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 3fa802ae92..64f4be1da7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1792,9 +1792,6 @@ expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buf
 }
 
 expr parser::parse_pattern_or_expr(unsigned rbp) {
-    if (m_in_quote) {
-        throw parser_error("patterns cannot occur inside of quoted terms", pos());
-    }
     all_id_local_scope scope(*this);
     return parse_expr(rbp);
 }