diff --git a/tex/paper.tex b/tex/paper.tex
index cb0f764be6e48d0af1cee66a7562836fe855bd8b..9968e02f38af7fad8c4700d088679eceac0d20cb 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -14,9 +14,7 @@
 %\usepackage{appendix}
 
 \usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
-% \addbibresource{../../fr-macros/rabe.bib}
-% \addbibresource{../../fr-macros/systems.bib}
-% \addbibresource{../../fr-macros/pub_rabe.bib}
+
 \addbibresource{kwarcpubs.bib}
 \addbibresource{extpubs.bib}
 \addbibresource{kwarccrossrefs.bib}
diff --git a/tex/viewfinder.tex b/tex/viewfinder.tex
index d71c357db41706ce9630db55a5506ed54a945296..dd647878c039414bd34ba42c34aa9e99f23242d2 100644
--- a/tex/viewfinder.tex
+++ b/tex/viewfinder.tex
@@ -4,7 +4,7 @@ To run a proper unficiation algorithm is in our situation infeasible, since the
 
 \paragraph{} We do so by first transforming each constant $C$ in a theory to an \emph{encoding} $(\cn{h}(C),\cn{syms}(C))$ the following way:
 
-Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by considering them like a separate set of variables, replacing them by their De Brujin indices and storing the symbol's names in a list $\cn{syms}(C)$. 
+Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by enumerating them and storing the symbol's names in a list $\cn{syms}(C)$. 
 
 As a result, we get a pair $(\cn{tree}(C),\cn{syms}(C))$. Now an assignment $V(C)=D$ is valid, iff $\cn{tree}(C)=\cn{tree}(D)$, the lists $\cn{syms}(C)$ and $\cn{syms}(D)$ have the same length and their pairwise assignments $V(\cn{syms}(C)_i)=\cn{syms}(D)_i$ are all valid.