equal
deleted
inserted
replaced
226 end |
226 end |
227 |
227 |
228 (* builds the aggregate equivalence relation *) |
228 (* builds the aggregate equivalence relation *) |
229 (* that will be the argument of Respects *) |
229 (* that will be the argument of Respects *) |
230 |
230 |
231 (* FIXME: check that the types correspond to each other? *) |
231 (* FIXME: check that the types correspond to each other *) |
232 fun equiv_relation ctxt (rty, qty) = |
232 fun equiv_relation ctxt (rty, qty) = |
233 if rty = qty |
233 if rty = qty |
234 then HOLogic.eq_const rty |
234 then HOLogic.eq_const rty |
235 else |
235 else |
236 case (rty, qty) of |
236 case (rty, qty) of |