--- a/Pearl-jv/Paper.thy	Fri Jul 23 16:42:47 2010 +0200
+++ b/Pearl-jv/Paper.thy	Sun Jul 25 22:42:21 2010 +0200
@@ -353,7 +353,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}