src/HOL/Tools/Quotient/quotient_term.ML

         matches trm_subst
       end
 
 (* generate type and term substitutions out of the
    qtypes involved in a quotient; the direction flag 
-   indicates in which direction the substitution work: 
+   indicates in which direction the substitutions work: 
    
      true:  quotient -> raw
      false: raw -> quotient
 *)
 fun mk_ty_subst qtys direction ctxt =

    |> map (if direction then swap else I)
 
 fun mk_trm_subst qtys direction ctxt =
 let
   val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
-  fun proper (t1, t2) = (subst_typ' (fastype_of t1) = fastype_of t2)
+  fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
 
   val const_substs = 
     Quotient_Info.qconsts_dest ctxt
      |> map (fn x => (#rconst x, #qconst x))
      |> map (if direction then swap else I)