diff -r aa960d16570f -r b1f55dd64481 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 19:52:46 2010 +0100
@@ -431,7 +431,7 @@
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
         if (member (op=) xs h)
         then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
+        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm 
   | _ => Conv.all_conv ctrm
 
 fun fun_map_conv xs ctxt ctrm =