Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.