diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -56,7 +56,7 @@
       yamllint .travis.yml
       yamllint .hlint.yaml
       yamllint .stylish-haskell.yaml
-      curl -sL https://raw.github.com/ndmitchell/hlint/master/misc/travis.sh | sh -s src app test bench
+      curl -sL https://raw.github.com/ndmitchell/hlint/master/misc/travis.sh | sh -s src app test/ bench
       curl -sL https://raw.github.com/ndmitchell/weeder/master/misc/travis.sh | sh -s .
     else
       echo "skipping yaml verification..."
diff --git a/ats-format.cabal b/ats-format.cabal
--- a/ats-format.cabal
+++ b/ats-format.cabal
@@ -1,5 +1,5 @@
 name:                ats-format
-version:             0.1.0.10
+version:             0.1.0.11
 synopsis:            A source-code formatter for ATS
 description:         An opinionated source-code formatter for ATS (http://www.ats-lang.org/).
 homepage:            https://hub.darcs.net/vmchale/ats-format#readme
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
@@ -318,12 +318,16 @@
      | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }
      | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- we do this because a $raise can have at most one argument
 
+StaticArgs : StaticExpression { [$1] }
+           | StaticArgs comma StaticExpression { $3 : $1 }
+
 StaticExpression : Name { StaticVal $1 }
                  | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }
                  | intLit { StaticInt $1 }
                  | boolLit { StaticBool $1 }
                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions
-
+                 | Name openParen StaticArgs closeParen { SCall $1 $3 }
+    
 -- | Parse an expression that can be called without parentheses
 PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $1) $3 }
               | Literal { $1 }
@@ -363,7 +367,7 @@
               | let openParen {% Left $ Expected $1 "Declaration" "(" }
 
 -- | Parse a termetric
-Termetric : openTermetric Expression closeTermetric { ($1, $2) }
+Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) }
           | underscore {% Left $ Expected $1 "_" "Name" }
           | dollar {% Left $ Expected $1 "$" "Name" }
 
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
@@ -219,11 +219,12 @@
 instance Pretty StaticExpression where
     pretty = cata a where
         a (StaticValF n)            = pretty n
-        a (StaticBinaryF op se se') = se <+> pretty op <+> se'
+        a (StaticBinaryF op se se') = se <> pretty op <> se'
         a (StaticIntF i)            = pretty i
         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
         a (StaticBoolF True)        = "true"
         a (StaticBoolF False)       = "false"
+        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))
 
 instance Pretty Type where
     pretty = cata a where
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -192,6 +192,7 @@
                       | StaticInt Int
                       | StaticBool Bool
                       | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)
+                      | SCall Name [StaticExpression]
                       deriving (Show, Eq, Generic, NFData)
 
 -- | A (possibly effectful) expression.
@@ -276,7 +277,7 @@
                         , universals    :: [Universal] -- ^ Universal quantifiers/refinement type
                         , args          :: [Arg] -- ^ Actual function arguments
                         , returnType    :: Type -- ^ Return type
-                        , termetric     :: Maybe Expression -- ^ Optional termination metric
+                        , termetric     :: Maybe StaticExpression -- ^ Optional termination metric
                         , expression    :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)
                         }
                         deriving (Show, Eq, Generic, NFData)