642 fun matches_bound v t = |
642 fun matches_bound v t = |
643 (case t of |
643 (case t of |
644 Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' |
644 Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' |
645 | _ => false); |
645 | _ => false); |
646 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false); |
646 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false); |
647 fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P; |
647 fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P; |
648 |
648 |
649 fun tr' q = (q, |
649 fun tr' q = (q, |
650 fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _), |
650 fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T), |
651 Const (c, _) $ (Const (d, _) $ t $ u) $ P] => |
651 Const (c, _) $ (Const (d, _) $ t $ u) $ P] => |
652 (case AList.lookup (op =) trans (q, c, d) of |
652 (case AList.lookup (op =) trans (q, c, d) of |
653 NONE => raise Match |
653 NONE => raise Match |
654 | SOME (l, g) => |
654 | SOME (l, g) => |
655 if matches_bound v t andalso not (contains_var v u) then mk v l u P |
655 if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P |
656 else if matches_bound v u andalso not (contains_var v t) then mk v g t P |
656 else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P |
657 else raise Match) |
657 else raise Match) |
658 | _ => raise Match); |
658 | _ => raise Match); |
659 in [tr' All_binder, tr' Ex_binder] end |
659 in [tr' All_binder, tr' Ex_binder] end |
660 *} |
660 *} |
661 |
661 |