Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quotient/quotient_tacs.ML
changeset 40469 f208cb239da1
parent 38865 43c934dd4bc3
child 40602 91e583511113 
--- 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 =
isabelle