--- 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