From 61578a84b6ca37dcc11d310eeff317ecf79bf448 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Tue, 25 Feb 2020 14:09:33 +0000
Subject: [PATCH] default is a keyword now

---
 src/Idris/Parser.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 9678d25..b86caae 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1007,7 +1007,7 @@ directive fname indents
          e <- extension
          atEnd indents
          pure (Extension e)
-  <|> do exactIdent "default"
+  <|> do keyword "default"
          tot <- totalityOpt
          atEnd indents
          pure (DefaultTotality tot)