Deduction theorem with undischarged statement I am reading "Mathematical logic" by Ian chriswell and Hodges and at one point in the text they mention 
the deductive theorem (page 17) which states; 
If $\Gamma \cup \left \{ \phi \right \} \vdash \psi $ then $\Gamma \vdash (\phi \rightarrow \psi)  \quad$
where  $\Gamma$ is the set containing the undischarged assumptions of the argument. Now my confusion starts at the point where they mention that its possible that $\phi \in \Gamma$ in which case it will still be an assumption in $\Gamma \vdash (\phi \rightarrow \psi)  \quad$ however I was under the impression that the whole point of the deduction theorem was to enable us to discharge assumptions so that they no longer are apart of $\Gamma$,  so what exactly is going on in this particular case? Is $\phi$ discharged or not?  
The author also mentions that the rule is still correctly applied if we do not discharge all occurrences of $\phi$ which does not seem like a correct statement for a rule whose purpose is to discharge assumptions.
 A: We can discharge the assumption $\phi$, but we are not forced to do so.
See page 17 :

Thus if $\phi$ is an assumption written somewhere in $D$, then we discharge $\phi$
  by writing a "dandah" through it: $\phi^/$. In the rule ($\to$I) below, and in similar rules later, the $\phi$ means that in forming the derivation we are allowed to discharge [emphasis mine] any occurrences of the assumption $\phi$ written in $D$.
The rule is still correctly applied if we do not discharge all of them [emphasis mine]; in fact the rule is correctly applied even if $\phi$ is not an assumption of $D$ at all, so that there is nothing to discharge.

You have also to note that [page 17] :

We shall discharge occurrences of assumptions.

Again, we can discharge all occurrences of an assumption $\phi$ but we are not forced to do it: we can discharge some occurrences of $\phi$ but not all. In this way, after the "discharge" the set $\Gamma$ of assumption may still include occurrences of $\phi$.

The "idea" of an undischarged assumption is simply this : if we can prove $\vdash \varphi \to \psi$ (without assumption) we can also prove : $\sigma \vdash \varphi \to \psi$ (with an extra-assumption).
Intuitively, a "redundant" assumption does not invalidate the proof of a theorem.
