--- a/src/HOL/Relation.thy Mon Feb 21 10:42:29 2011 +0100
+++ b/src/HOL/Relation.thy Mon Feb 21 10:44:19 2011 +0100
@@ -132,7 +132,7 @@
lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
by blast
-lemma Id_on_def'[nitpick_def, code]:
+lemma Id_on_def' [nitpick_unfold, code]:
"(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
by (auto simp add: fun_eq_iff
elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
@@ -227,7 +227,7 @@
lemma refl_on_Id_on: "refl_on A (Id_on A)"
by (rule refl_onI [OF Id_on_subset_Times Id_onI])
-lemma refl_on_def'[nitpick_def, code]:
+lemma refl_on_def' [nitpick_unfold, code]:
"refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)