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 \ \x. P x"
-restricted definition "induct_implies A B \ A \ B"
-restricted definition "induct_equal x y \ x = y"
-restricted definition "induct_conj A B \ A \ B"
-restricted definition "induct_true \ True"
-restricted definition "induct_false \ False"
+qualified definition "induct_forall P \ \x. P x"
+qualified definition "induct_implies A B \ A \ B"
+qualified definition "induct_equal x y \ x = y"
+qualified definition "induct_conj A B \ A \ B"
+qualified definition "induct_true \ True"
+qualified definition "induct_false \ False"
lemma induct_forall_eq: "(\x. P x) \ Trueprop (induct_forall (\x. P x))"
by (unfold atomize_all induct_forall_def)