src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Fri Jan 27 19:08:48 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Sat Jan 28 06:13:03 2012 +0100
@@ -615,13 +615,6 @@
 
 lemmas acc_subset_induct = accp_subset_induct [to_set]
 
-text {* Very basic code generation setup *}
-
-declare accp.simps[code]
-
-lemma [code_unfold]:
-  "(x : acc r) = accp (%x xa. (x, xa) : r) x"
-by (simp add: accp_acc_eq)
 
 subsection {* Tools for building wellfounded relations *}