# HG changeset patch
# User blanchet
# Date 1280157962 -7200
# Node ID 12a559b5c55045489245eea9b236e271f3854a49
# Parent  f1b7fb87f5231350b89c575d6bd42e275c7c504a
simplify code

diff -r f1b7fb87f523 -r 12a559b5c550 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:22:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:26:02 2010 +0200
@@ -171,13 +171,9 @@
 
 fun make_axiom_clauses thy clauses = fold_rev (add_axiom_clause thy) clauses []
 
-fun make_conjecture_clauses thy =
-  let
-    (* ### FIXME: kill "aux" *)
-    fun aux _ [] = []
-      | aux n (t :: ts) =
-        make_clause thy (n, "conjecture", Conjecture, t) :: aux (n + 1) ts
-  in aux 0 end
+fun make_conjecture_clauses thy ts =
+  map2 (fn j => fn t => make_clause thy (j, "conjecture", Conjecture, t))
+       (0 upto length ts - 1) ts
 
 (** Helper clauses **)