1417 val (rhead, rargs) = strip_comb rtrm |
1417 val (rhead, rargs) = strip_comb rtrm |
1418 val (qhead, qargs) = strip_comb qtrm |
1418 val (qhead, qargs) = strip_comb qtrm |
1419 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
1419 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
1420 in |
1420 in |
1421 if rty = qty |
1421 if rty = qty |
1422 then list_comb (rhead, rargs') |
1422 then |
|
1423 case (rhead, qhead) of |
|
1424 (Free (_, T), Free (_, T')) => |
|
1425 if T = T' then list_comb (rhead, rargs') |
|
1426 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
|
1427 | _ => list_comb (rhead, rargs') |
1423 else |
1428 else |
1424 case (rhead, qhead, length rargs') of |
1429 case (rhead, qhead, length rargs') of |
1425 (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead |
1430 (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead |
1426 | (Free _, Free _, 0) => mk_repabs lthy (rty, qty) rhead |
1431 | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead |
1427 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
1432 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
1428 | (Free (x, T), Free (x', T'), _) => |
1433 | (Free (x, T), Free (x', T'), _) => |
1429 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
1434 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
1430 | (Abs _, Abs _, _ ) => |
1435 | (Abs _, Abs _, _ ) => |
1431 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |
1436 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |