# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277800643 -3600
# Node ID ebc157ab01b09b3580650597a93672c2c2d5ed34
# Parent  165cd386288dabff2bf3f7c470b04877c485fe39
tuned

diff -r 165cd386288d -r ebc157ab01b0 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Jun 29 07:55:18 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Jun 29 09:37:23 2010 +0100
@@ -734,7 +734,7 @@
 
 (* 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
@@ -748,7 +748,7 @@
 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