diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -2888,8 +2888,8 @@
   and   X::"('a::pt_name) set set"
   and   pi2::"coname prm"
   and   Y::"('b::pt_coname) set set"
-  shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
-  and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
+  shows "(pi1\<bullet>(\<Inter>X)) = \<Inter>(pi1\<bullet>X)"
+  and   "(pi2\<bullet>(\<Inter>Y)) = \<Inter>(pi2\<bullet>Y)"
 apply(auto simp add: perm_set_def)
 apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
 apply(perm_simp)