diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
index da86d38..e55447e 100644
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.lhs
@@ -565,7 +565,7 @@ Apply a function to a list of arguments
 >       fPrec x (RBind n (B Pi t) sc) 
 >           | nameOccurs n sc = bracket x 2 $
 >              "("++forget n ++":"++fPrec 10 t++") -> " ++ fPrec 10 sc
->           | otherwise = bracket x 2
+>           | otherwise = bracket x 2 $
 >              (fPrec 1 t) ++" -> " ++ fPrec 10 sc
 >       fPrec x (RBind n (B (Let v) t) sc) = bracket x 2 $
 >           "let "++forget n ++":"++ fPrec 10 t
diff --git a/papers/ivor/corett.tex b/papers/ivor/corett.tex
index f038f3a..bf1de7e 100644
--- a/papers/ivor/corett.tex
+++ b/papers/ivor/corett.tex
@@ -36,7 +36,9 @@ \subsection{The Core Calculus}
 functional programming languages, we may also write the function space
 \mbox{$\all{\vx}{\vS}\SC\vT$} as \mbox{$\fbind{\vx}{\vS}{\vT}$}, or
 abbreviate it to \mbox{$\vS\to\vT$} if $\vx$ is not free in
-$\vT$. Contexts ($\Gamma$) are defined inductively; the empty context
+$\vT$. 
+Universe levels on types ($\Type_i$) may be left implicit.
+Contexts ($\Gamma$) are defined inductively; the empty context
 is valid, as is a context extended with a $\lambda$, $\forall$ or
 $\LET$ binding:
 
diff --git a/papers/ivor/ivor.tex b/papers/ivor/ivor.tex
index 0cd4b45..b4ae7a8 100644
--- a/papers/ivor/ivor.tex
+++ b/papers/ivor/ivor.tex
@@ -70,7 +70,8 @@
 
 \section*{Acknowledgements}
 
-This work is generously supported by EPSRC grant EP/C001346/1.
+This work is generously supported by EPSRC grant EP/C001346/1. My thanks to
+\ldots
 
 \bibliographystyle{abbrv}
 \begin{small}
diff --git a/papers/ivor/tactics.tex b/papers/ivor/tactics.tex
index 28fe08b..637af76 100644
--- a/papers/ivor/tactics.tex
+++ b/papers/ivor/tactics.tex
@@ -121,7 +121,7 @@ \subsection{Basic Tactics}
 
 A tactic operates on a hole binding, specified by the \texttt{Goal}
 argument. This can be a named binding, \texttt{goal :: Name -> Goal},
-or the default goal \texttt{defaultGoal::Name}. The default goal is
+or the default goal \texttt{defaultGoal :: Goal}. The default goal is
 the first goal generated by the most recent tactic application.
 
 \mysubsubsection{Hole Manipulations}