equal
deleted
inserted
replaced
175 |
175 |
176 fun instance consts (c, Ts) = |
176 fun instance consts (c, Ts) = |
177 let |
177 let |
178 val declT = declaration consts c; |
178 val declT = declaration consts c; |
179 val vars = map Term.dest_TVar (typargs consts (c, declT)); |
179 val vars = map Term.dest_TVar (typargs consts (c, declT)); |
180 in declT |> Term.instantiateT (vars ~~ Ts) end; |
180 in declT |> TermSubst.instantiateT (vars ~~ Ts) end; |
181 |
181 |
182 |
182 |
183 |
183 |
184 (** build consts **) |
184 (** build consts **) |
185 |
185 |