--- a/Pearl-jv/Paper.thy	Mon Feb 28 15:21:10 2011 +0000
+++ b/Pearl-jv/Paper.thy	Mon Feb 28 16:47:13 2011 +0000
@@ -3,7 +3,7 @@
 imports "../Nominal/Nominal2_Base" 
         "../Nominal/Nominal2_Eqvt"
         "../Nominal/Atoms" 
-        "../Nominal/Abs"
+        "../Nominal/Nominal2_Abs"
         "LaTeXsugar"
 begin
 
@@ -314,7 +314,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 a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} 
+  @{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}