116 val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) |
116 val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) |
117 |
117 |
118 fun convert_eqs (f, qs, gs, args, rhs) = |
118 fun convert_eqs (f, qs, gs, args, rhs) = |
119 let |
119 let |
120 val MutualPart {i, i', ...} = get_part f parts |
120 val MutualPart {i, i', ...} = get_part f parts |
|
121 val rhs' = rhs |
|
122 |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) |
121 in |
123 in |
122 (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), |
124 (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), |
123 SumTree.mk_inj RST n' i' (replace_frees rews rhs) |
125 Envir.beta_norm (SumTree.mk_inj RST n' i' rhs')) |
124 |> Envir.beta_norm) |
|
125 end |
126 end |
126 |
127 |
127 val qglrs = map convert_eqs fqgars |
128 val qglrs = map convert_eqs fqgars |
128 in |
129 in |
129 Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, |
130 Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, |