--- a/thys/Paper/Paper.thy	Mon Mar 14 23:08:58 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 15 01:10:38 2016 +0000
@@ -744,8 +744,8 @@
 
   \begin{theorem}\mbox{}\smallskip\\
   \begin{tabular}{ll}
-  (1) & @{thm (lhs) lex_correct1a} if and only if @{thm (rhs) lex_correct1a}\\
-  (2) & @{thm (lhs) lex_correct3b} if and only if @{thm (rhs) lex_correct3b}\\
+  (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\
+  (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\
   \end{tabular}
   \end{theorem}