src/HOL/Product_Type.thy
changeset 18220 43cf5767f992
parent 18013 3f5d0acdfdba
child 18328 841261f303a1
equal deleted inserted replaced
18219:6c84210902db 18220:43cf5767f992
   863        | _ => NONE)
   863        | _ => NONE)
   864   | _ => NONE);
   864   | _ => NONE);
   865 
   865 
   866 in
   866 in
   867 
   867 
   868 val prod_codegen_setup =
   868 val prod_codegen_setup = [
   869   [Codegen.add_codegen "let_codegen" let_codegen,
   869   Codegen.add_codegen "let_codegen" let_codegen,
   870    Codegen.add_codegen "split_codegen" split_codegen];
   870   Codegen.add_codegen "split_codegen" split_codegen,
       
   871   CodegenPackage.add_codegen_expr
       
   872     ("let", CodegenPackage.codegen_let strip_abs),
       
   873   CodegenPackage.add_codegen_expr
       
   874     ("split", CodegenPackage.codegen_split strip_abs)
       
   875 ];
   871 
   876 
   872 end;
   877 end;
   873 *}
   878 *}
   874 
   879 
   875 setup prod_codegen_setup
   880 setup prod_codegen_setup