equal
deleted
inserted
replaced
703 (* CB: frozen_tvars has the following type: |
703 (* CB: frozen_tvars has the following type: |
704 ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *) |
704 ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *) |
705 |
705 |
706 fun frozen_tvars ctxt Ts = |
706 fun frozen_tvars ctxt Ts = |
707 let |
707 let |
708 val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts)); |
708 val tvars = rev (fold Term.add_tvarsT Ts []); |
709 val tfrees = map TFree |
709 val tfrees = map TFree |
710 (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); |
710 (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); |
711 in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end; |
711 in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end; |
712 |
712 |
713 fun unify_frozen ctxt maxidx Ts Us = |
713 fun unify_frozen ctxt maxidx Ts Us = |