# HG changeset patch
# User haftmann
# Date 1133535912 -3600
# Node ID a41ce9c10b738bbcbdeed006a347c138823f8467
# Parent  b356f783792190eb70024bee7774a6b2a30bdbfd
adjusted to improved code generator interface

diff -r b356f7837921 -r a41ce9c10b73 src/HOL/Integ/IntDef.thy
--- 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]
diff -r b356f7837921 -r a41ce9c10b73 src/HOL/Product_Type.thy
--- 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;
diff -r b356f7837921 -r a41ce9c10b73 src/HOL/Tools/datatype_codegen.ML
--- 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;