--- a/Nominal/Abs.thy	Mon Mar 15 09:27:25 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 15 10:02:19 2010 +0100
@@ -110,7 +110,10 @@
   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
-  oops
+  apply(simp add: c[symmetric])
+  apply(subst permute_eqvt[symmetric])
+  apply simp
+  done
 
 fun
   alpha_abs