From ba1ea599d803a169e9635db455f74ba68d4faf69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Fri, 21 Feb 2020 19:03:45 +0000
Subject: [PATCH] Fix rendering of rule labels in mathpar

---
 macros.tex | 13 +++++++------
 thesis.tex |  6 +++---
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/macros.tex b/macros.tex
index 150f3c5..ab67bd5 100644
--- a/macros.tex
+++ b/macros.tex
@@ -99,12 +99,13 @@
 %% Labels
 %%
 \newcommand{\slab}[1]{\textrm{#1}}
-\newcommand{\klab}[1]{\textrm{K-#1}}
-\newcommand{\semlab}[1]{\textrm{S-#1}}
-\newcommand{\tylab}[1]{\textrm{T-#1}}
-\newcommand{\mlab}[1]{\text{\scshape{M-#1}}}
-\newcommand{\siglab}[1]{\text{\scshape{Sig-#1}}}
-\newcommand{\rowlab}[1]{\text{\scshape{R-#1}}}
+\newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
+\newcommand{\klab}[1]{\rulelabel{K}{#1}}
+\newcommand{\semlab}[1]{\rulelabel{S}{#1}}
+\newcommand{\tylab}[1]{\rulelabel{T}{#1}}
+\newcommand{\mlab}[1]{\rulelabel{M}{#1}}
+\newcommand{\siglab}[1]{\rulelabel{Sig}{#1}}
+\newcommand{\rowlab}[1]{\rulelabel{R}{#1}}
 
 %%
 %% Syntactic categories.
diff --git a/thesis.tex b/thesis.tex
index 81e4bc7..2b7e274 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -868,9 +868,9 @@ that the binder $x : A$.
 \semlab{App}   & (\lambda x^A . \, M) V &\reducesto& M[V/x] \\
 \semlab{TyApp} & (\Lambda \alpha^K . \, M) A &\reducesto& M[A/\alpha] \\
 \semlab{Split} & \Let \; \Record{\ell = x;y} = \Record{\ell = V;W} \; \In \; N &\reducesto& N[V/x,W/y] \\
-\semlab{Case$_1$} &
+\semlab{Case_1} &
   \Case \; (\ell~V)^R \{ \ell \; x \mapsto M; y \mapsto N\} &\reducesto& M[V/x] \\
-\semlab{Case$_2$} &
+\semlab{Case_2} &
   \Case \; (\ell~V)^R \{ \ell' \; x \mapsto M; y \mapsto N\} &\reducesto& N[(\ell~V)^R/y], \hfill\quad \text{if } \ell \neq \ell' \\
 \semlab{Let} &
   \Let \; x \revto \Return \; V \; \In \; N &\reducesto& N[V/x] \\
@@ -986,7 +986,7 @@ some label $\ell$ binds the payload $V$ to $x$ and the remainder $W$
 to $y$ in the continuation $N$.
 %
 Disjunctive case splitting is handled by the two rules
-\semlab{Case$_1$} and \semlab{Case$_2$}. The former rule handles the
+\semlab{Case_1} and \semlab{Case_2}. The former rule handles the
 success case, when the scrutinee's tag $\ell$ matches the tag of the
 success clause, thus binds the payload $V$ to $x$ and proceeds to
 evaluate the continuation $M$. The latter rule handles the