# HG changeset patch
# User haftmann
# Date 1158672111 -7200
# Node ID 527563e67194306f89463eb05b251b1ab0a76b7c
# Parent  7cbb224598b25ab009d55df6cf4ad881128760d9
dropped error-prone code generation 2 for wfrec

diff -r 7cbb224598b2 -r 527563e67194 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Tue Sep 19 15:21:48 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue Sep 19 15:21:51 2006 +0200
@@ -291,13 +291,6 @@
 fun wfrec f x = f (wfrec f) x;
 *}
 
-setup {*
-  CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
-*}
-
-code_const wfrec
-  (SML target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
-  (Haskell target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
 
 subsection{*Variants for TFL: the Recdef Package*}