src/HOL/Tools/Metis/metis_translate.ML
changeset 43174 f497a1e97d37
parent 43173 b98daa96d043
child 43175 4ca344fe0aca
equal deleted inserted replaced
43173:b98daa96d043 43174:f497a1e97d37
    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) =