--- a/src/HOL/Integ/IntDef.thy Fri Dec 02 16:04:48 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy Fri Dec 02 16:05:12 2005 +0100
@@ -915,8 +915,8 @@
setup {*[
Codegen.add_codegen "number_of_codegen" number_of_codegen,
- CodegenPackage.add_codegen_expr
- ("number", CodegenPackage.codegen_number_of HOLogic.dest_binum mk_int_to_nat)
+ CodegenPackage.add_appgen
+ ("number", CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat)
]*}
quickcheck_params [default_type = int]
--- a/src/HOL/Product_Type.thy Fri Dec 02 16:04:48 2005 +0100
+++ b/src/HOL/Product_Type.thy Fri Dec 02 16:05:12 2005 +0100
@@ -868,10 +868,10 @@
val prod_codegen_setup = [
Codegen.add_codegen "let_codegen" let_codegen,
Codegen.add_codegen "split_codegen" split_codegen,
- CodegenPackage.add_codegen_expr
- ("let", CodegenPackage.codegen_let strip_abs),
- CodegenPackage.add_codegen_expr
- ("split", CodegenPackage.codegen_split strip_abs)
+ CodegenPackage.add_appgen
+ ("let", CodegenPackage.appgen_let strip_abs),
+ CodegenPackage.add_appgen
+ ("split", CodegenPackage.appgen_split strip_abs)
];
end;
--- a/src/HOL/Tools/datatype_codegen.ML Fri Dec 02 16:04:48 2005 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Dec 02 16:05:12 2005 +0100
@@ -305,19 +305,16 @@
|> is_some;
fun get_datatype thy dtname =
- case CodegenPackage.tname_of_idf thy dtname
- of SOME dtname =>
- dtname
- |> Symtab.lookup (DatatypePackage.get_datatypes thy)
- |> Option.map #descr
- |> these
- |> get_first (fn (_, (dtname', vs, cs)) =>
- if dtname = dtname'
- then SOME (vs, map fst cs)
- else NONE)
- |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
- | _ => NONE;
-
+ dtname
+ |> Symtab.lookup (DatatypePackage.get_datatypes thy)
+ |> Option.map #descr
+ |> these
+ |> get_first (fn (_, (dtname', vs, cs)) =>
+ if dtname = dtname'
+ then SOME (vs, map fst cs)
+ else NONE)
+ |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)));
+
fun get_datacons thy (c, dtname) =
let
val descr =
@@ -358,11 +355,13 @@
CodegenPackage.set_is_datatype
is_datatype,
CodegenPackage.add_defgen
- ("datatype", CodegenPackage.defgen_datatype get_datatype),
+ ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
CodegenPackage.add_defgen
("datacons", CodegenPackage.defgen_datacons get_datacons),
- CodegenPackage.add_codegen_expr
- ("case", CodegenPackage.codegen_case get_case_const_data)
+ CodegenPackage.add_defgen
+ ("dataeq", CodegenPackage.defgen_datatype_eqinst get_datatype),
+ CodegenPackage.add_appgen
+ ("case", CodegenPackage.appgen_case get_case_const_data)
];
end;