equal
deleted
inserted
replaced
1372 *} |
1372 *} |
1373 |
1373 |
1374 (* rep-abs injection *) |
1374 (* rep-abs injection *) |
1375 |
1375 |
1376 ML {* |
1376 ML {* |
1377 (* FIXME: is this the right get_fun function for rep-abs injection *) |
|
1378 fun mk_repabs lthy (T, T') trm = |
1377 fun mk_repabs lthy (T, T') trm = |
1379 Quotient_Def.get_fun repF lthy (T, T') |
1378 Quotient_Def.get_fun repF lthy (T, T') |
1380 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
1379 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
1381 *} |
1380 *} |
1382 |
1381 |
1383 ML {* length *} |
|
1384 |
1382 |
1385 ML {* |
1383 ML {* |
1386 (* bound variables need to be treated properly, *) |
1384 (* bound variables need to be treated properly, *) |
1387 (* as the type of subterms need to be calculated *) |
1385 (* as the type of subterms need to be calculated *) |
1388 |
1386 |