# HG changeset patch
# User bulwahn
# Date 1327727583 -3600
# Node ID b159ca4e268bda94c9e3584cbd14fc99ec84d0a2
# Parent  ee500921279317aa1f2f1c8b2c32668d7685d7c3
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code

diff -r ee5009212793 -r b159ca4e268b 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 *}