diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 5072bdc..3e3a71f 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -306,7 +306,7 @@ mutual
       <|> [|TYPE universe|]
       <|> Nat  <$ resC "ℕ"
       <|> Zero <$ resC "zero"
-      <|> (nat <&> \n => fromNat n :# Nat)
+      <|> [|fromNat nat|]
       <|> [|V name|]
       <|> [|Tag tag|]
 
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index 4776ea2..6ca28fd 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -229,7 +229,7 @@ tests = "parser" :- [
     parsesAs term "Nat" Nat,
     parsesAs term "zero" Zero,
     parsesAs term "succ n" (Succ $ V "n"),
-    parsesAs term "3" (Succ (Succ (Succ Zero)) :# Nat),
+    parsesAs term "3" (Succ (Succ (Succ Zero))),
     parseFails term "succ"
   ],
 
@@ -237,8 +237,8 @@ tests = "parser" :- [
     parsesAs term "[1.ℕ]" $ BOX One Nat,
     parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat),
     parsesAs term "[a]" $ Box (V "a"),
-    parsesAs term "[0]" $ Box (Zero :# Nat),
-    parsesAs term "[1]" $ Box (Succ Zero :# Nat)
+    parsesAs term "[0]" $ Box Zero,
+    parsesAs term "[1]" $ Box (Succ Zero)
   ],
 
   "case" :- [
@@ -274,7 +274,7 @@ tests = "parser" :- [
         CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"),
     parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $
       Case Any (V "n") (Nothing, Nat) $
-        CaseNat (Zero :# Nat) (Nothing, One, Just "ih", V "ih"),
+        CaseNat Zero (Nothing, One, Just "ih", V "ih"),
     parseFails term "caseω n return A of { zero ⇒ a }",
     parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
   ],