src/HOL/Product_Type.thy
changeset 18220 43cf5767f992
parent 18013 3f5d0acdfdba
child 18328 841261f303a1
--- a/src/HOL/Product_Type.thy	Tue Nov 22 12:42:59 2005 +0100
+++ b/src/HOL/Product_Type.thy	Tue Nov 22 12:59:25 2005 +0100
@@ -865,9 +865,14 @@
 
 in
 
-val prod_codegen_setup =
-  [Codegen.add_codegen "let_codegen" let_codegen,
-   Codegen.add_codegen "split_codegen" split_codegen];
+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)
+];
 
 end;
 *}