src/HOL/Fun.thy
changeset 40968 a6fcd305f7dc
parent 40719 acb830207103
child 40969 fb2d3ccda5a7
--- a/src/HOL/Fun.thy	Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 06 09:19:10 2010 +0100
@@ -126,7 +126,7 @@
   "map_fun f g h x = g (h (f x))"
   by (simp add: map_fun_def)
 
-type_mapper map_fun
+type_lifting map_fun
   by (simp_all add: fun_eq_iff)