Quot/quotient_term.ML
changeset 796 64f9c76f70c7
parent 795 a28f805df355
child 797 35436401f00d
--- a/Quot/quotient_term.ML	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 26 23:20:46 2009 +0100
@@ -228,7 +228,7 @@
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 
-(* FIXME: check that the types correspond to each other? *)
+(* FIXME: check that the types correspond to each other *)
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty