diff -r b0b30df60056 -r 93ec303e1917 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 16:38:36 2011 +0200
@@ -17,7 +17,7 @@
 
   datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
-  datatype format = CNF_UEQ | FOF | TFF | THF
+  datatype format = CNF | CNF_UEQ | FOF | TFF | THF
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
     Decl of string * 'a * 'a ho_type |
@@ -71,6 +71,8 @@
   val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
   val is_format_typed : format -> bool
   val tptp_strings_for_atp_problem : format -> string problem -> string list
+  val ensure_cnf_problem :
+    (string * string) problem -> (string * string) problem
   val filter_cnf_ueq_problem :
     (string * string) problem -> (string * string) problem
   val declare_undeclared_syms_in_atp_problem :
@@ -99,7 +101,7 @@
 
 datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
-datatype format = CNF_UEQ | FOF | TFF | THF
+datatype format = CNF | CNF_UEQ | FOF | TFF | THF
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
   Decl of string * 'a * 'a ho_type |
@@ -256,7 +258,8 @@
 val default_source =
   ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
 
-fun string_for_format CNF_UEQ = tptp_cnf
+fun string_for_format CNF = tptp_cnf
+  | string_for_format CNF_UEQ = tptp_cnf
   | string_for_format FOF = tptp_fof
   | string_for_format TFF = tptp_tff
   | string_for_format THF = tptp_thf
@@ -306,6 +309,8 @@
     Formula (ident, Hypothesis, mk_anot phi, source, info)
   | negate_conjecture_line line = line
 
+fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line))
+
 fun filter_cnf_ueq_problem problem =
   problem
   |> map (apsnd (map open_formula_line