--- a/LMCS-Paper/Paper.thy	Fri Dec 23 15:04:01 2011 +0000
+++ b/LMCS-Paper/Paper.thy	Thu Dec 29 12:37:38 2011 +0000
@@ -854,7 +854,7 @@
   "abs\<^bsub>set\<^esub>"} we have
 
   \begin{equation}\label{abseqiff}
-  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 
+  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 
   @{term "alpha_set_ex (as, x) equal supp (bs, y)"}
   \end{equation}\smallskip