1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -30,8 +30,10 @@
     1.4    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
     1.5    datatype 'a problem_line =
     1.6      Decl of string * 'a * 'a ho_type |
     1.7 -    Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
     1.8 -               * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
     1.9 +    Formula of string * formula_kind
    1.10 +               * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    1.11 +               * (string, string ho_type) ho_term option
    1.12 +               * (string, string ho_type) ho_term option
    1.13    type 'a problem = (string * 'a problem_line list) list
    1.14  
    1.15    val tptp_cnf : string