src/HOL/Nominal/nominal_inductive.ML

--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -47,8 +47,7 @@
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
-      | _ => NONE),
-    identifier = []};
+      | _ => NONE)};
 
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);