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