src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Datatype.thy	Fri May 05 17:17:21 2006 +0200
@@ -6,7 +6,8 @@
 header {* Datatypes *}
 
 theory Datatype
-imports Datatype_Universe
+imports Datatype_Universe FunDef
+uses ("Tools/function_package/fundef_datatype.ML")
 begin
 
 subsection {* Representing primitive types *}
@@ -314,4 +315,9 @@
     ml (target_atom "SOME")
     haskell (target_atom "Just")
 
+
+use "Tools/function_package/fundef_datatype.ML"
+setup FundefDatatype.setup
+
+
 end