src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Mon Dec 06 09:19:10 2010 +0100
+++ b/src/HOL/Datatype.thy	Mon Dec 06 09:25:05 2010 +0100
@@ -13,6 +13,12 @@
   ("Tools/Datatype/datatype_realizer.ML")
 begin
 
+subsection {* Prelude: lifting over function space *}
+
+type_lifting map_fun
+  by (simp_all add: fun_eq_iff)
+
+
 subsection {* The datatype universe *}
 
 typedef (Node)