adding case theorems for code generator
authorhaftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 198185c5c1208a3fa
parent 19817 bb16bf9ae3fd
child 19819 14de4d05d275
adding case theorems for code generator
src/HOL/Tools/datatype_codegen.ML
     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 #>