1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -981,8 +981,8 @@
     1.4                      else I)
     1.5                in
     1.6                  t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
     1.7 -                  |> make_formula thy format type_sys true (string_of_int j)
     1.8 -                                  General kind
     1.9 +                  |> make_formula thy format type_sys (format <> CNF)
    1.10 +                                  (string_of_int j) General kind
    1.11                    |> maybe_negate
    1.12                end)
    1.13           (0 upto last) ts