equal
deleted
inserted
replaced
643 (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) |
643 (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) |
644 in |
644 in |
645 cls_str :: (typ_clss 0 tfree_lits) |
645 cls_str :: (typ_clss 0 tfree_lits) |
646 end; |
646 end; |
647 |
647 |
648 fun clause_info cls = |
648 fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls); |
649 let |
|
650 val cls_id = string_of_clauseID cls |
|
651 val ax_name = string_of_axiomName cls |
|
652 in |
|
653 ((ax_name^""), cls_id) |
|
654 end; |
|
655 |
649 |
656 |
650 |
657 fun clause2tptp cls = |
651 fun clause2tptp cls = |
658 let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
652 let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
659 val cls_id = string_of_clauseID cls |
653 val cls_id = string_of_clauseID cls |