src/HOL/Product_Type.thy
changeset 20105 454f4be984b7
parent 20044 92cc2f4c7335
child 20380 14f9f2a1caa6
--- a/src/HOL/Product_Type.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -842,12 +842,10 @@
   | _ => NONE);
 
 val prod_codegen_setup =
-  Codegen.add_codegen "let_codegen" let_codegen #>
-  Codegen.add_codegen "split_codegen" split_codegen #>
-  CodegenPackage.add_appconst
-    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #>
-  CodegenPackage.add_appconst
-    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split));
+  Codegen.add_codegen "let_codegen" let_codegen
+  #> Codegen.add_codegen "split_codegen" split_codegen
+  #> CodegenPackage.add_appconst
+       ("Let", CodegenPackage.appgen_let)
 
 *}