# HG changeset patch
# User haftmann
# Date 1149692139 -7200
# Node ID 5c5c1208a3fa53137f7e9bed7f755378f5a9227f
# Parent  bb16bf9ae3fd06979f8bc3ed58f2da753f43da89
adding case theorems for code generator

diff -r bb16bf9ae3fd -r 5c5c1208a3fa src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Jun 07 16:55:14 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jun 07 16:55:39 2006 +0200
@@ -337,6 +337,13 @@
       ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
   end;
 
+fun add_datatype_case_defs dtco thy =
+  let
+    val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
+  in
+    fold CodegenTheorems.add_fun case_rewrites thy
+  end;
+
 val setup = 
   add_codegen "datatype" datatype_codegen #>
   add_tycodegen "datatype" datatype_tycodegen #>