Mercurial Mercurial > hg > nominal2 / 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.
Quot/quotient_tacs.ML
changeset 913 b1f55dd64481
parent 911 95ee248b3832
child 920 dae99175f584 
--- 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 =
nominal2