From 8c50efeb7530fde387d015578b7dfa246e2c996b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 23 Feb 2017 01:31:44 +0100
Subject: [PATCH] refactor(init/meta/lean/parser): simplify sep_by

---
 library/init/meta/lean/parser.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean
index 72f779a4e1..d18526a29c 100644
--- a/library/init/meta/lean/parser.lean
+++ b/library/init/meta/lean/parser.lean
@@ -57,11 +57,10 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
            return $ y::ys) <|> pure list.nil
 
 local postfix ?:100 := optional
-local notation p ` ?: `:100 d := (λ o, option.get_or_else o d) <$> p?
 local postfix * := many
 
 meta def sep_by {α : Type} : string → parser α → parser (list α)
-| s p := (list.cons <$> p <*> (tk s *> p)*) ?: []
+| s p := (list.cons <$> p <*> (tk s *> p)*) <|> return []
 
 end parser
 end lean