--- a/Pearl/Paper.thy	Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl/Paper.thy	Wed Mar 02 00:06:28 2011 +0000
@@ -1,7 +1,6 @@
 (*<*)
 theory Paper
 imports "../Nominal/Nominal2_Base" 
-        "../Nominal/Nominal2_Eqvt" 
         "../Nominal/Atoms" 
         "LaTeXsugar"
 begin
@@ -346,7 +345,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 minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}