--- a/Nominal/Nominal2_Base.thy	Sun Aug 14 08:52:03 2011 +0200
+++ b/Nominal/Nominal2_Base.thy	Mon Aug 15 10:43:22 2011 +0200
@@ -1015,7 +1015,7 @@
 
 instance 
 apply(default)
-unfolding Inf_fun_def
+unfolding Inf_fun_def INF_def
 apply(perm_simp)
 apply(rule refl)
 done