--- a/Pearl/Paper.thy	Fri Jul 23 16:41:36 2010 +0200
+++ b/Pearl/Paper.thy	Fri Jul 23 16:42:00 2010 +0200
@@ -347,7 +347,7 @@
   @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
   @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
   @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
-  @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} 
+  @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}