diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,5 +1,5 @@
 name:                language-ats
-version:             0.1.1.19
+version:             0.1.1.20
 synopsis:            Parser and pretty-printer for ATS.
 description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.
 license:             BSD3
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -481,13 +481,9 @@
                | Expression { Right $1 }
 
 -- | Parse the details of an implementation
-Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 (Right $9) }
-               | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] (Right $7) }
-               | Universals FunName MaybeImplicit Universals eq Expression { Implement $5 $1 $3 $4 $2 [NoArgs] (Right $6) }
+Implementation : Universals FunName MaybeImplicit Universals FunArgs eq Expression { Implement $6 $1 $3 $4 $2 $5 (Right $7) }
 
-StaticImplementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq StaticExpression { Implement $5 $1 $3 $4 $2 $6 (Left $9) }
-                     | Universals FunName MaybeImplicit Universals doubleParens eq StaticExpression { Implement $5 $1 $3 $4 $2 [] (Left $7) }
-                     | Universals FunName MaybeImplicit Universals eq StaticExpression { Implement $5 $1 $3 $4 $2 [NoArgs] (Left $6) }
+StaticImplementation : Universals FunName MaybeImplicit Universals FunArgs eq StaticExpression { Implement $6 $1 $3 $4 $2 $5 (Left $7) }
 
 -- | Parse a function name
 FunName : IdentifierOr { Unqualified $1 }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -293,7 +293,7 @@
         a (Vt0pF ad)              = "vt@ype" <> pretty ad
         a (AtF _ (Just t) t')     = t <+> "@" <+> t'
         a (AtF _ Nothing t)       = "@" <> t
-        a (ProofTypeF _ t t')     = parens (prettyArgsU "" "" t <+> "|" <+> t')
+        a (ProofTypeF _ t t')     = parens (prettyArgsG "" "" t <+> "|" <+> t')
         a (ConcreteTypeF e)       = pretty e
         a (TupleF _ ts)           = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
         a (RefTypeF t)            = "&" <> t
diff --git a/test/data/fastcount.out b/test/data/fastcount.out
--- a/test/data/fastcount.out
+++ b/test/data/fastcount.out
@@ -20,7 +20,7 @@
 fun rawmemchr {l:addr}{m:int}( pf : bytes_v(l, m) | p : ptr(l)
                              , c : int
                              ) : [ l2 : addr | l+m > l2 ] ( bytes_v(l, l2-l)
-                                                          ,bytes_v(l2, l+m-l2)
+                                                          , bytes_v(l2, l+m-l2)
                                                            | ptr(l2)) =
   "mac#atslib_rawmemchr"