Я пытаюсь определить новую команду определения типа для Изабель из FOL.Этот новый тип "T" должен иметь вид "T::term", но я не нахожу никакой функции для этого в Pure.
Я следовал идеям typedef.ML из HOL.
Без этой сортировки (сортировка по умолчанию) я не получаю унификацию сортировок между аксиомами, которые я определяю.