--- 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"
--- 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
--- 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;