697 in foldl rename_aT ([],vars) end; |
697 in foldl rename_aT ([],vars) end; |
698 |
698 |
699 fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); |
699 fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); |
700 |
700 |
701 |
701 |
|
702 (* left-ro-right traversal *) |
|
703 |
|
704 (*foldl atoms of type*) |
|
705 fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts) |
|
706 | foldl_atyps f x_atom = f x_atom; |
|
707 |
|
708 (*foldl atoms of term*) |
|
709 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u) |
|
710 | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t) |
|
711 | foldl_aterms f x_atom = f x_atom; |
|
712 |
|
713 (*foldl types of term*) |
|
714 fun foldl_types f (x, Const (_, T)) = f (x, T) |
|
715 | foldl_types f (x, Free (_, T)) = f (x, T) |
|
716 | foldl_types f (x, Var (_, T)) = f (x, T) |
|
717 | foldl_types f (x, Bound _) = x |
|
718 | foldl_types f (x, Abs (_, T, t)) = foldl_types f (f (x, T), t) |
|
719 | foldl_types f (x, t $ u) = foldl_types f (foldl_types f (x, t), u); |
|
720 |
|
721 |
702 |
722 |
703 (*** Compression of terms and types by sharing common subtrees. |
723 (*** Compression of terms and types by sharing common subtrees. |
704 Saves 50-75% on storage requirements. As it is fairly slow, |
724 Saves 50-75% on storage requirements. As it is fairly slow, |
705 it is called only for axioms, stored theorems, etc. ***) |
725 it is called only for axioms, stored theorems, etc. ***) |
706 |
726 |