584 let |
584 let |
585 val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; |
585 val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; |
586 fun rewrite _ _ = |
586 fun rewrite _ _ = |
587 let |
587 let |
588 fun subst (Abs (v, T, b)) = Abs (v, T, subst b) |
588 fun subst (Abs (v, T, b)) = Abs (v, T, subst b) |
589 | subst (t as _ $ _) = |
589 | subst t = |
590 let val (u, vs) = strip_comb t in |
590 let val (u, vs) = strip_comb t in |
591 if is_Free u andalso has_call u then |
591 if is_Free u andalso has_call u then |
592 Const (@{const_name Inr}, dummyT) $ |
592 Const (@{const_name Inr}, dummyT) $ |
593 (try (foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y)) vs |
593 (if null vs then HOLogic.unit |
594 |> the_default (hd vs)) |
594 else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs) |
595 else if try (fst o dest_Const) u = SOME @{const_name prod_case} then |
595 else if try (fst o dest_Const) u = SOME @{const_name prod_case} then |
596 list_comb (u |> map_types (K dummyT), map subst vs) |
596 list_comb (u |> map_types (K dummyT), map subst vs) |
597 else |
597 else |
598 list_comb (subst u, map subst vs) |
598 list_comb (subst u, map subst vs) |
599 end |
599 end; |
600 | subst t = t; |
|
601 in |
600 in |
602 subst |
601 subst |
603 end; |
602 end; |
604 fun massage rhs_term t = massage_indirect_corec_call |
603 fun massage rhs_term t = massage_indirect_corec_call |
605 lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term; |
604 lthy has_call rewrite [] (range_type (fastype_of t)) rhs_term; |