diff -r 847972b7b5ba -r 27aab7a105eb Nominal/nominal_inductive.ML
--- 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
         [] => ()