600 |
600 |
601 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
601 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
602 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
602 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
603 |
603 |
604 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
604 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
605 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
605 let |
|
606 val rty = fastype_of rtrm |
|
607 val qty = fastype_of qtrm |
|
608 in |
|
609 mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) |
|
610 end |
606 |
611 |
607 | (Abs (x, T, t), Abs (x', T', t')) => |
612 | (Abs (x, T, t), Abs (x', T', t')) => |
608 let |
613 let |
609 val rty = fastype_of rtrm |
614 val rty = fastype_of rtrm |
610 val qty = fastype_of qtrm |
615 val qty = fastype_of qtrm |