--- a/thys/Paper/Paper.thy	Thu Apr 28 11:17:16 2016 +0100
+++ b/thys/Paper/Paper.thy	Wed May 04 11:29:37 2016 +0100
@@ -857,7 +857,7 @@
   \end{center}
 
   \noindent
-  The functions @{text "simp\<^bsub>ALT\<^esub>"} and @{text "simp\<^bsub>SEQ\<^esub>"} encode the simplification rules
+  The functions @{text "simp\<^bsub>Alt\<^esub>"} and @{text "simp\<^bsub>Seq\<^esub>"} encode the simplification rules
   and compose the rectification functions. The main simplification function is then 
 
   \begin{center}