# HG changeset patch
# User haftmann
# Date 1289307734 -3600
# Node ID f208cb239da152b68fb6f5744fce0751b41cf757
# Parent  d4aac200199e49399480b40ebce36f2286184ab1
slightly changed fun_map_def

diff -r d4aac200199e -r f208cb239da1 src/HOL/Tools/Quotient/quotient_tacs.ML
--- 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 =