Cleanup. Change intro example

introduction.tex

@@ -146,24 +146,24 @@ We prove soundness and aim for a good compromise between completeness and time c
 \begin{figure}
 \begin{minipage}{0.43\textwidth}
 \begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
-genBox() {
+genList() {
-    if( ... ) {
+  if( ... ) {
-        return new Box(1);
+    return new List(1);
-    } else {
+  } else {
-        return new Box("Str");
+    return new List("Str");
-    }
+  }
 }
     \end{lstlisting}
 \end{minipage}%
 \hfill
 \begin{minipage}{0.55\textwidth}
 \begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
-Box<?> genBox() {
+List<?> genList() {
-    if( ... ) {
+  if( ... ) {
-        return new Box<Integer>(1);
+    return new List<Integer>(1);
-    } else {
+  } else {
-        return new Box<String>("Str");
+    return new List<String>("Str");
-    }
+  }
 }
     \end{lstlisting}
 \end{minipage}

unify.tex

@@ -252,7 +252,7 @@ whereas \rulename{Clear} and \rulename{Exclude} remove wildcard placeholders or
 allow the constraint to be processed by \rulename{Prepare}.
 
 \subsection{Adding Wildcards to the mix}
-\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
+%\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
 %Input constraints originating from a completely untyped input program do not contain any existential types.
 %Those are added during \unify{}.
 Wildcard types are added preemptively and if necessary can be removed later down the line.
@@ -264,8 +264,6 @@ results in $\tv{a} \doteq \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard
 The upper and lower bounds of the freshly generated wildcard $\rwildcard{X}$ are type placeholders.
 If a second constraint like $\tv{a} \lessdot \exptype{List}{\type{String}}$
 exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and upper bound to $\type{String}$.
-
-\textit{Example:}
 \begin{displaymath}
 \prftree[r]{\rulename{Reduce}}{
 \prftree[r]{\rulename{Subst}}{
@@ -283,15 +281,16 @@ exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and
 %Wildcards are bound to a type.
 % and can therefore only be created at T <. a constraints
 % After a reduce step the information to which Type the wildcard was bound is lost!
-\begin{lstlisting}
+% \begin{lstlisting}
-<X> List<X> concat(List<X> l, List<X> r){ ... }
+% <X> List<X> concat(List<X> l, List<X> r){ ... }
 
-someList(){
+% someList(){
-  return new List("String") :? new List(42);
+%   return new List("String") :? new List(42);
-}
+% }
-\end{lstlisting}
+% \end{lstlisting}
 
-Constraints for the untyped \texttt{someList} method:
+Take the introduction example from listing \ref{lst:intro-example}.
+Constraints for the untyped \texttt{genList} method:
 \begin{constraintset}
 $\begin{array}{l}
 \exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}},