--- a/thys/Paper/Paper.thy	Sun Mar 13 01:07:34 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Mar 14 15:15:29 2016 +0000
@@ -892,7 +892,7 @@
   it (that is construct @{term "f\<^sub>r v"}). We can prove that
 
   \begin{lemma}
-  @{term "slexer r s = lexer r s"}
+  @{thm slexer_correctness}
   \end{lemma}
 
   \noindent