1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:22:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:26:02 2010 +0200
     1.3 @@ -171,13 +171,9 @@
     1.4  
     1.5  fun make_axiom_clauses thy clauses = fold_rev (add_axiom_clause thy) clauses []
     1.6  
     1.7 -fun make_conjecture_clauses thy =
     1.8 -  let
     1.9 -    (* ### FIXME: kill "aux" *)
    1.10 -    fun aux _ [] = []
    1.11 -      | aux n (t :: ts) =
    1.12 -        make_clause thy (n, "conjecture", Conjecture, t) :: aux (n + 1) ts
    1.13 -  in aux 0 end
    1.14 +fun make_conjecture_clauses thy ts =
    1.15 +  map2 (fn j => fn t => make_clause thy (j, "conjecture", Conjecture, t))
    1.16 +       (0 upto length ts - 1) ts
    1.17  
    1.18  (** Helper clauses **)
    1.19