reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
--- 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 *}