src/HOL/Tools/ATP/atp_translate.ML

   update_combformula (formula_map
       (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
 
 (** Helper facts **)
 
-(* The Boolean indicates that a fairly sound type encoding is needed. *)
+(* The Boolean indicates that a fairly sound type encoding is needed.
+   "false" must precede "true" to ensure consistent numbering and a correct
+   mapping in Metis. *)
 val helper_table =
   [("COMBI", (false, @{thms Meson.COMBI_def})),
    ("COMBK", (false, @{thms Meson.COMBK_def})),
    ("COMBB", (false, @{thms Meson.COMBB_def})),
    ("COMBC", (false, @{thms Meson.COMBC_def})),

     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
        However, this is done so for backward compatibility: Including the
        equality helpers by default in Metis breaks a few existing proofs. *)
     (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
                   fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    ("fFalse", (true, @{thms True_or_False})),
-   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
+   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    ("fTrue", (true, @{thms True_or_False})),
-   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    ("fNot",
     (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
                    fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    ("fconj",
     (false,