diff -r f101eac348f8 -r 1fd7388360b6 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Paper/Paper.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -791,7 +791,7 @@
   value returned by the lexer must be unique.   A simple corollary 
   of our two theorems is:
 
-  \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
+  \begin{corollary}\mbox{}\smallskip\\\label{lexercorrectcor}
   \begin{tabular}{ll}
   (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 
   (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\