diff -r 5574138cf97c -r a81dc82ecba3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Apr 09 15:54:09 2015 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 09 20:42:32 2015 +0200
@@ -1377,12 +1377,12 @@
 context
 begin
 
-restricted definition "induct_forall P \<equiv> \<forall>x. P x"
-restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal x y \<equiv> x = y"
-restricted definition "induct_conj A B \<equiv> A \<and> B"
-restricted definition "induct_true \<equiv> True"
-restricted definition "induct_false \<equiv> False"
+qualified definition "induct_forall P \<equiv> \<forall>x. P x"
+qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal x y \<equiv> x = y"
+qualified definition "induct_conj A B \<equiv> A \<and> B"
+qualified definition "induct_true \<equiv> True"
+qualified definition "induct_false \<equiv> False"
 
 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)