Added datatype_case.

--- a/src/HOL/Inductive.thy	Tue Apr 24 15:18:09 2007 +0200
+++ b/src/HOL/Inductive.thy	Tue Apr 24 15:18:42 2007 +0200
@@ -18,6 +18,7 @@
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_realizer.ML")
   ("Tools/datatype_hooks.ML")
+  ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
   ("Tools/recfun_codegen.ML")
@@ -113,6 +114,7 @@
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"
 use "Tools/datatype_abs_proofs.ML"
+use "Tools/datatype_case.ML"
 use "Tools/datatype_realizer.ML"
 
 use "Tools/datatype_hooks.ML"