src/HOL/Tools/datatype_codegen.ML
changeset 19818 5c5c1208a3fa
parent 19599 a5c7eb37d14f
child 19886 6bec6daac280
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jun 07 16:55:14 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jun 07 16:55:39 2006 +0200
     1.3 @@ -337,6 +337,13 @@
     1.4        ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
     1.5    end;
     1.6  
     1.7 +fun add_datatype_case_defs dtco thy =
     1.8 +  let
     1.9 +    val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
    1.10 +  in
    1.11 +    fold CodegenTheorems.add_fun case_rewrites thy
    1.12 +  end;
    1.13 +
    1.14  val setup = 
    1.15    add_codegen "datatype" datatype_codegen #>
    1.16    add_tycodegen "datatype" datatype_tycodegen #>