src/HOL/Code_Setup.thy

--- a/src/HOL/Code_Setup.thy	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:54:44 2007 +0200
@@ -127,11 +127,6 @@
 
 lemmas [code func] = Let_def if_True if_False
 
-setup {*
-  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
-  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
-*}
-
 
 subsection {* Evaluation oracle *}
 
@@ -160,5 +155,4 @@
       THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"
 
-
 end