# HG changeset patch # User Cezary Kaliszyk # Date 1265728208 -3600 # Node ID 26f15c2dc131d0a981bf1f0cfd3a0611b1f307fd # Parent 5eb84b817855c420060ccd95835af3813bb3e4ab removing unnecessary brackets diff -r 5eb84b817855 -r 26f15c2dc131 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Feb 09 15:55:58 2010 +0100 +++ b/Quot/quotient_tacs.ML Tue Feb 09 16:10:08 2010 +0100 @@ -246,7 +246,7 @@ in case (bare_concl, qt_asm) of (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => - if (fastype_of qt_fun) = (fastype_of f) + if fastype_of qt_fun = fastype_of f then no_tac else let @@ -426,7 +426,7 @@ fun fun_map_simple_conv xs ctrm = case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => - if (member (op=) xs h) + if member (op=) xs h then Conv.all_conv ctrm else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm | _ => Conv.all_conv ctrm