equal
deleted
inserted
replaced
575 | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) |
575 | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) |
576 | string_of_term (Fun (name,typ,[])) = name |
576 | string_of_term (Fun (name,typ,[])) = name |
577 | string_of_term (Fun (name,typ,terms)) = |
577 | string_of_term (Fun (name,typ,terms)) = |
578 let val terms' = map string_of_term terms |
578 let val terms' = map string_of_term terms |
579 in |
579 in |
580 if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms')) |
580 if (!keep_types) then name ^ (ResLib.list_to_string (terms' @ [typ])) |
581 else name ^ (ResLib.list_to_string terms') |
581 else name ^ (ResLib.list_to_string terms') |
582 end; |
582 end; |
583 |
583 |
584 |
584 |
585 |
585 |
588 fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
588 fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
589 | string_of_predicate (Predicate(name,_,[])) = name |
589 | string_of_predicate (Predicate(name,_,[])) = name |
590 | string_of_predicate (Predicate(name,typ,terms)) = |
590 | string_of_predicate (Predicate(name,typ,terms)) = |
591 let val terms_as_strings = map string_of_term terms |
591 let val terms_as_strings = map string_of_term terms |
592 in |
592 in |
593 if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) |
593 if (!keep_types) |
|
594 then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) |
594 else name ^ (ResLib.list_to_string terms_as_strings) |
595 else name ^ (ResLib.list_to_string terms_as_strings) |
595 end; |
596 end; |
596 |
597 |
597 |
598 |
598 |
599 |