diff --git a/spec/doc.tex b/spec/doc.tex
index a3b860f82be7a286ed4fe4667a0de0b191bfcd2f..3979a025a6ed219ca9ef08b78a9c6de95c02769b 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1073,24 +1073,44 @@ remove the steps of the subproof from memory after checking it.
 \end{comment}
 
 \subsection*{Sharing and Skolem Terms}
-The proof output generated by veriT is generally large. One reason
-for this is that veriT can store terms internally much more efficiently.
-By utilizing a perfect sharing data structure, every term is stored in
-memory precisely once. When printing the proof this compact storage
-is unfolded.
-
-The user of veriT can optionally activate sharing\footnote{By using
-the command-line option \texttt{--proof-with-sharing}.} to print common
+Alethe proofs are generally large. One reason for this is that SMT
+solvers can store terms internally much more efficiently.  A term data
+structure with perfect sharing ensures that every term is stored in memory
+precisely once. When printing the proof this compact storage is unfolded.
+
+Alethe can optionally use sharing\footnote{For veriT this can be activated
+by the command-line option \texttt{--proof-with-sharing}.} to print common
 subterms only once.  This is realized using the standard naming mechanism
 of SMT-LIB. In the language of SMT-LIB it is possible to annotate any
 term $t$ with a name $n$ by writing $\grT{(! }t\grT{ :named }n\grT{ )}$
 where $n$ is a symbol. After a term is annotated with a name, the name can
 be used in place of the term. This is a purely syntactical replacement.
-
-To simplify reconstruction veriT can optionally\footnote{By using the
-command-line option \texttt{--proof-define-skolems}.} define Skolem
-constants as functions. If activated, this option adds a list of
-$\grT{define-fun}$ command to define shorthand 0-ary functions for
+Alethe continues to use the names already used in the input problem.
+Hence, terms that already have a name in the input problem can be replaced
+by that name and new names introduced in the proof must not use names
+already used in the input problem.
+
+To limit the number of names introduced, an SMT solver can use the following
+simple approach used by veriT.
+Before printing the proof it iterates over all terms of the proof and
+recursively descend into the terms. It marks every unmarked subterm it
+visits. If a visited term is already marked, the solver assigns a new name
+to this term.  If a term already has a name, it does not descend further
+into the term.
+%
+By doing so, it ensures that only terms that appear as
+child of two different parent terms get a name.  Since a name term is replaced
+with its name after it first appearance, a term that only appears
+as a child of one single term not need a distinct name.
+%
+Thanks to the perfect
+sharing representation testing if a term is marked takes constant time
+and the overall traversal takes linear time in the proof size.
+
+To simplify reconstruction Alethe can optionally\footnote{For veriT by
+using the command-line option \texttt{--proof-define-skolems}.} define
+Skolem constants as functions. In this case the proof contains a list
+of $\grT{define-fun}$ commands that define shorthand 0-ary functions for
 the $\grT{(choice }\dots\grT{)}$ terms needed. Without this option,
 no $\grT{define-fun}$ commands are issued and the constants are expanded.