slightly changed fun_map_def

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Nov 09 14:02:14 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Nov 09 14:02:14 2010 +0100
@@ -434,7 +434,7 @@
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
         if member (op=) xs h
         then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
+        else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
   | _ => Conv.all_conv ctrm
 
 fun fun_map_conv xs ctxt ctrm =