equal
deleted
inserted
replaced
601 | Free (a, _) => Name.declare a |
601 | Free (a, _) => Name.declare a |
602 | _ => I) tm #> |
602 | _ => I) tm #> |
603 declare_tfree_names tm; |
603 declare_tfree_names tm; |
604 |
604 |
605 fun variant_frees t frees = |
605 fun variant_frees t frees = |
606 #1 (fold_map Name.variant (map fst frees) (Name.build_context (declare_term_names t))) ~~ |
606 Name.variant_names_build (declare_term_names t) frees; |
607 map #2 frees; |
|
608 |
607 |
609 |
608 |
610 (* sorts *) |
609 (* sorts *) |
611 |
610 |
612 fun smash_sortsT_same S' = |
611 fun smash_sortsT_same S' = |