src/HOL/Tools/datatype_codegen.ML
changeset 22429 09e794384323
parent 22423 c1836b14c63a
child 22435 16e6ddc30f92
equal deleted inserted replaced
22428:1755e6381b2c 22429:09e794384323
   523       in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
   523       in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
   524 
   524 
   525 
   525 
   526 (* registering code types in code generator *)
   526 (* registering code types in code generator *)
   527 
   527 
   528 val codetype_hook =
   528 fun codetype_hook x =
   529   fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec));
   529   fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)) x;
   530 
   530 
   531 
   531 
   532 (* instrumentalizing the sort algebra *)
   532 (* instrumentalizing the sort algebra *)
   533 
   533 
   534 (*fun assume_arities_of_sort thy arities ty_sort =
   534 (*fun assume_arities_of_sort thy arities ty_sort =