# HG changeset patch
# User haftmann
# Date 1324738389 -3600
# Node ID 76cf71ed15c7b2347ca12c5f9f33801325ec86bb
# Parent  03ce2b2a29a20a26473dcaef72b8ab3babd5a795
dropped obsolete code equation for Id

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 (\<lambda>(x, y). x = y \<and> A x)"
 by auto