1signature Thm = 2sig 3 4 include FinalThm where type tag = Tag.tag 5 and type hol_type = Type.hol_type 6 and type term = Term.term 7end 8