equal
deleted
inserted
replaced
173 |
173 |
174 The matching is necessary for types like |
174 The matching is necessary for types like |
175 |
175 |
176 ('a * 'a) list / 'a bar |
176 ('a * 'a) list / 'a bar |
177 |
177 |
178 The test is necessary in order to eliminate superflous |
178 The test is necessary in order to eliminate superfluous |
179 identity maps. |
179 identity maps. |
180 *) |
180 *) |
181 |
181 |
182 fun absrep_fun flag ctxt (rty, qty) = |
182 fun absrep_fun flag ctxt (rty, qty) = |
183 if rty = qty |
183 if rty = qty |
356 A = B ----> (R ===> R) A B |
356 A = B ----> (R ===> R) A B |
357 |
357 |
358 for more complicated types of A and B |
358 for more complicated types of A and B |
359 *) |
359 *) |
360 |
360 |
361 |
|
362 val mk_babs = Const (@{const_name Babs}, dummyT) |
361 val mk_babs = Const (@{const_name Babs}, dummyT) |
363 val mk_ball = Const (@{const_name Ball}, dummyT) |
362 val mk_ball = Const (@{const_name Ball}, dummyT) |
364 val mk_bex = Const (@{const_name Bex}, dummyT) |
363 val mk_bex = Const (@{const_name Bex}, dummyT) |
365 val mk_resp = Const (@{const_name Respects}, dummyT) |
364 val mk_resp = Const (@{const_name Respects}, dummyT) |
366 |
365 |