diff -r 7d46aa03696e -r 087d81f5213e src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 22:11:01 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Apr 06 23:14:05 2015 +0200
@@ -14,7 +14,7 @@
 structure NominalInductive : NOMINAL_INDUCTIVE =
 struct
 
-val inductive_forall_def = @{thm induct_forall_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};