From b7e79dea29634c47e2ae722e25b9efaeb6ffa600 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Oct 2015 21:01:22 -0700
Subject: [PATCH] fix(frontends/lean/parser): bug in parse_double

---
 src/frontends/lean/parser.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 3bd05df6f..e6723a1e1 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -696,7 +696,9 @@ unsigned parser::parse_small_nat() {
 double parser::parse_double() {
     if (curr() != scanner::token_kind::Decimal)
         throw parser_error("decimal value expected", pos());
-    return get_num_val().get_double();
+    double r =get_num_val().get_double();
+    next();
+    return r;
 }
 
 static level lift(level l, unsigned k) {