diff -r ee19cdb07528 -r c1836b14c63a src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Fri Mar 09 08:45:50 2007 +0100
+++ b/src/HOL/Code_Generator.thy	Fri Mar 09 08:45:53 2007 +0100
@@ -87,7 +87,9 @@
   (Haskell infixl 4 "==")
 
 
-text {* boolean expressions *}
+text {* type bool *}
+
+code_datatype True False
 
 lemma [code func]:
   shows "(False \<and> x) = False"
@@ -152,18 +154,22 @@
   bool true false not
 
 
-text {* itself as a code generator datatype *}
+text {* type prop *}
+
+code_datatype Trueprop "prop"
+
+
+text {* type itself *}
 
-setup {*
-  let
-    val v = ("'a", []);
-    val t = Logic.mk_type (TFree v);
-    val Const (c, ty) = t;
-    val (_, Type (dtco, _)) = strip_type ty;
-  in
-    CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
-  end
-*} 
+code_datatype "TYPE('a)"
+
+
+text {* prevent unfolding of quantifier definitions *}
+
+lemma [code func]:
+  "Ex = Ex"
+  "All = All"
+  by rule+
 
 
 text {* code generation for arbitrary as exception *}