1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 16:32:48 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 16:32:49 2011 +0200
     1.3 @@ -1335,8 +1335,10 @@
     1.4         equality helpers by default in Metis breaks a few existing proofs. *)
     1.5      @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
     1.6             fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
     1.7 -   (("fAll", false), []), (*TODO: add helpers*)
     1.8 -   (("fEx", false), []), (*TODO: add helpers*)
     1.9 +   (* Partial characterization of "fAll" and "fEx". A complete characterization
    1.10 +      would require the axiom of choice for replay with Metis. *)
    1.11 +   (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
    1.12 +   (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
    1.13     (("If", true), @{thms if_True if_False True_or_False})]
    1.14    |> map (apsnd (map zero_var_indexes))
    1.15  
    1.16 @@ -1740,7 +1742,7 @@
    1.17        [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
    1.18           (* We must add "bool" in case the helper "True_or_False" is added
    1.19              later. In addition, several places in the code rely on the list of
    1.20 -            nonmonotonic types not being empty. *)
    1.21 +            nonmonotonic types not being empty. (FIXME?) *)
    1.22           |> insert_type ctxt I @{typ bool}
    1.23      else
    1.24        []
    1.25 @@ -1889,10 +1891,7 @@
    1.26  
    1.27  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
    1.28                                       poly_nonmono_Ts type_enc sym_decl_tab =
    1.29 -  sym_decl_tab
    1.30 -  |> Symtab.dest
    1.31 -  |> sort_wrt fst
    1.32 -  |> rpair []
    1.33 +  sym_decl_tab |> Symtab.dest |> sort_wrt fst |> rpair []
    1.34    |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
    1.35                               nonmono_Ts poly_nonmono_Ts type_enc)
    1.36  
    1.37 @@ -1936,7 +1935,7 @@
    1.38        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
    1.39                         |> map repair
    1.40      val poly_nonmono_Ts =
    1.41 -      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
    1.42 +      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] (* FIXME? *) orelse
    1.43           polymorphism_of_type_enc type_enc <> Polymorphic then
    1.44          nonmono_Ts
    1.45        else