src/HOL/Tools/ATP/atp_translate.ML

     (* 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. *)
     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
-   (("fAll", false), []), (*TODO: add helpers*)
-   (("fEx", false), []), (*TODO: add helpers*)
+   (* Partial characterization of "fAll" and "fEx". A complete characterization
+      would require the axiom of choice for replay with Metis. *)
+   (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
+   (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
    (("If", true), @{thms if_True if_False True_or_False})]
   |> map (apsnd (map zero_var_indexes))
 
 val type_tag = `make_fixed_const type_tag_name
 

   let val level = level_of_type_enc type_enc in
     if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
       [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
          (* We must add "bool" in case the helper "True_or_False" is added
             later. In addition, several places in the code rely on the list of
-            nonmonotonic types not being empty. *)
+            nonmonotonic types not being empty. (FIXME?) *)
          |> insert_type ctxt I @{typ bool}
     else
       []
   end
 

                       conj_sym_kind poly_nonmono_Ts type_enc n s)
        end)
 
 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
                                      poly_nonmono_Ts type_enc sym_decl_tab =
-  sym_decl_tab
-  |> Symtab.dest
-  |> sort_wrt fst
-  |> rpair []
+  sym_decl_tab |> Symtab.dest |> sort_wrt fst |> rpair []
   |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
                              nonmono_Ts poly_nonmono_Ts type_enc)
 
 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
     poly <> Mangled_Monomorphic andalso

       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
                        |> map repair
     val poly_nonmono_Ts =
-      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
+      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] (* FIXME? *) orelse
          polymorphism_of_type_enc type_enc <> Polymorphic then
         nonmono_Ts
       else
         [tvar_a]
     val sym_decl_lines =