--- 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 

--- a/Nominal/nominal_inductive.ML	Sun Aug 14 08:52:03 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Mon Aug 15 10:43:22 2011 +0200
@@ -391,7 +391,7 @@
       hd names
       |> the o Induct.lookup_inductP ctxt
       |> fst o Rule_Cases.get
-      |> map fst
+      |> map (fst o fst)
 
     val _ = (case duplicates (op = o pairself fst) avoids of
         [] => ()