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