# HG changeset patch
# User haftmann
# Date 1191520486 -7200
# Node ID abcd15369ffa7e7cddad4c668739c3e4dd512a63
# Parent  98c006a30218c8a0304713788c179f13f40ac764
tuned datatype_codegen setup

diff -r 98c006a30218 -r abcd15369ffa src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Oct 04 19:54:44 2007 +0200
+++ b/src/HOL/Datatype.thy	Thu Oct 04 19:54:46 2007 +0200
@@ -10,6 +10,7 @@
 
 theory Datatype
 imports Finite_Set
+uses "Tools/datatype_codegen.ML"
 begin
 
 typedef (Node)
@@ -527,9 +528,6 @@
 by auto
 
 
-subsection {* Finishing the datatype package setup *}
-
-setup "DatatypeCodegen.setup_hooks"
 text {* hides popular names *}
 hide (open) type node item
 hide (open) const Push Node Atom Leaf Numb Lim Split Case
@@ -685,6 +683,8 @@
 
 subsubsection {* Code generator setup *}
 
+setup DatatypeCodegen.setup
+
 definition
   is_none :: "'a option \<Rightarrow> bool" where
   is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
diff -r 98c006a30218 -r abcd15369ffa src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Oct 04 19:54:44 2007 +0200
+++ b/src/HOL/Inductive.thy	Thu Oct 04 19:54:46 2007 +0200
@@ -17,7 +17,6 @@
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
-  ("Tools/datatype_codegen.ML")
   ("Tools/primrec_package.ML")
 begin
 
@@ -108,8 +107,6 @@
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
 use "Tools/primrec_package.ML"
-use "Tools/datatype_codegen.ML"
-setup DatatypeCodegen.setup
 
 use "Tools/inductive_codegen.ML"
 setup InductiveCodegen.setup
diff -r 98c006a30218 -r abcd15369ffa src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 04 19:54:44 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 04 19:54:46 2007 +0200
@@ -29,7 +29,6 @@
     -> theory -> theory
 
   val setup: theory -> theory
-  val setup_hooks: theory -> theory
 end;
 
 structure DatatypeCodegen : DATATYPE_CODEGEN =
@@ -433,6 +432,7 @@
     |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     |> Thm.implies_intr asm
     |> Thm.generalize ([], params) 0
+    |> Conv.fconv_rule (Class.unoverload thy)
     |> Thm.varifyT
   end;
 
@@ -587,13 +587,6 @@
 
 (** theory setup **)
 
-fun add_datatype_case_const dtco thy =
-  let
-    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
-  in
-    CodePackage.add_appconst (case_name, CodePackage.appgen_case dest_case_expr) thy
-  end;
-
 fun add_datatype_case_defs dtco thy =
   let
     val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
@@ -601,15 +594,15 @@
     fold_rev Code.add_default_func case_rewrites thy
   end;
 
+fun add_datatype_case_certs dtco thy =
+  Code.add_case (get_case_cert thy dtco) thy;
+
 val setup = 
   add_codegen "datatype" datatype_codegen
   #> add_tycodegen "datatype" datatype_tycodegen
-  #> DatatypePackage.interpretation (fold add_datatype_case_const)
+  #> DatatypePackage.interpretation (fold add_datatype_case_certs)
   #> DatatypePackage.interpretation (fold add_datatype_case_defs)
-
-val setup_hooks =
-  add_codetypes_hook codetype_hook
+  #> add_codetypes_hook codetype_hook
   #> add_codetypes_hook eq_hook
 
-
 end;