diff -r 7f589bfecffa -r ffe5d850df62 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Sat Feb 13 02:00:09 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Feb 15 21:48:57 2016 +0100
@@ -320,8 +320,7 @@
   \noindent
   which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "}
 
-  \item[(2)] This case is similar except that in the last step we have to
-  instantiate the existential quantifier with @{term "Seq (projval r\<^sub>1 c v) v'"}
+  \item[(2)] This case is similar.
   \end{itemize}
 
   \noindent