# HG changeset patch
# User haftmann
# Date 1219829069 -7200
# Node ID 2308843f8b66f7b4fc9380e9121e4f38860aa028
# Parent  90074908db1664f12802ea5ea2cf00e782740d92
tuned code generator setup

diff -r 90074908db16 -r 2308843f8b66 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Wed Aug 27 04:47:30 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Wed Aug 27 11:24:29 2008 +0200
@@ -74,7 +74,6 @@
 
 subsection {* Generic code generator setup *}
 
-
 text {* using built-in Haskell equality *}
 
 code_class eq
@@ -86,8 +85,6 @@
 
 text {* type bool *}
 
-lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
-
 code_type bool
   (SML "bool")
   (OCaml "bool")
@@ -113,17 +110,14 @@
 
 text {* code generation for undefined as exception *}
 
+code_abort undefined
+
 code_const undefined
   (SML "raise/ Fail/ \"undefined\"")
   (OCaml "failwith/ \"undefined\"")
   (Haskell "error/ \"undefined\"")
 
 
-text {* Let and If *}
-
-lemmas [code func] = Let_def if_True if_False
-
-
 subsection {* Evaluation oracle *}
 
 ML {*
diff -r 90074908db16 -r 2308843f8b66 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 27 04:47:30 2008 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 27 11:24:29 2008 +0200
@@ -1659,10 +1659,17 @@
 
 subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
 
-code_datatype Trueprop "prop"
+setup {*
+  Code.map_pre (K HOL_basic_ss)
+  #> Code.map_post (K HOL_basic_ss)
+*}
+
+code_datatype True False
 
 code_datatype "TYPE('a\<Colon>{})"
 
+code_datatype Trueprop "prop"
+
 lemma Let_case_cert:
   assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   shows "CASE x \<equiv> f x"
@@ -1718,6 +1725,9 @@
   shows "\<not> True \<longleftrightarrow> False"
     and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
 
+lemmas [code func] = Let_def if_True if_False
+
+lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
 
 
 subsection {* Legacy tactics and ML bindings *}