49 val metis_generated_var_prefix = "_" |
49 val metis_generated_var_prefix = "_" |
50 |
50 |
51 val metis_name_table = |
51 val metis_name_table = |
52 [((tptp_equal, 2), (metis_equal, false)), |
52 [((tptp_equal, 2), (metis_equal, false)), |
53 ((tptp_old_equal, 2), (metis_equal, false)), |
53 ((tptp_old_equal, 2), (metis_equal, false)), |
54 ((const_prefix ^ predicator_name, 1), (metis_predicator, false)), |
54 ((prefixed_predicator_name, 1), (metis_predicator, false)), |
55 ((prefixed_app_op_name, 2), (metis_app_op, false)), |
55 ((prefixed_app_op_name, 2), (metis_app_op, false)), |
56 ((prefixed_type_tag_name, 2), (metis_type_tag, true))] |
56 ((prefixed_type_tag_name, 2), (metis_type_tag, true))] |
57 |
57 |
58 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) |
58 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) |
59 | predicate_of thy (t, pos) = |
59 | predicate_of thy (t, pos) = |