diff -r 03ce2b2a29a2 -r 76cf71ed15c7 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Sat Dec 24 15:53:09 2011 +0100 +++ b/src/HOL/Relation.thy Sat Dec 24 15:53:09 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_unfold, code]: +lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\(x, y). x = y \ A x)" by auto