tuned

--- a/src/HOL/Code_Generator.thy	Fri Apr 20 16:55:38 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Apr 20 17:58:24 2007 +0200
@@ -164,14 +164,6 @@
 code_datatype "TYPE('a)"
 
 
-text {* prevent unfolding of quantifier definitions *}
-
-lemma [code func]:
-  "Ex = Ex"
-  "All = All"
-  by rule+
-
-
 text {* code generation for undefined as exception *}
 
 code_const undefined