diff -r 67b78d5dea5b -r f247fc952f31 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 23:59:36 2011 +0200
@@ -36,7 +36,7 @@
 
 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
 
-val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_bool = mk_meta_eq @{thm perm_bool_def};
 val perm_boolI = @{thm perm_boolI};
 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   (Drule.strip_imp_concl (cprop_of perm_boolI))));