# HG changeset patch
# User blanchet
# Date 1280176357 -7200
# Node ID 523dc7ad6f9f0d647a212fd98296e7fa4bd6710c
# Parent  31705eccee23136b9fdafb86c167a20919d2329a
simplify code

diff -r 31705eccee23 -r 523dc7ad6f9f src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:22:23 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:32:37 2010 +0200
@@ -233,11 +233,8 @@
                 ctypes_sorts = ctypes_sorts}
   end
 
-fun add_axiom_clause thy (name, th) =
-  cons (name, make_clause thy (0, name, Axiom, prop_of th))
-
-fun make_axiom_clauses thy clauses = fold_rev (add_axiom_clause thy) clauses []
-
+fun make_axiom_clause thy (name, th) =
+  (name, make_clause thy (0, name, Axiom, prop_of th))
 fun make_conjecture_clauses thy ts =
   map2 (fn j => fn t => make_clause thy (j, "conjecture", Conjecture, t))
        (0 upto length ts - 1) ts
@@ -267,9 +264,8 @@
   Symtab.make (maps (maps (map (rpair 0) o fst))
                     [optional_helpers, optional_typed_helpers])
 
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
+fun get_helper_clauses thy is_FO full_types conjectures axclauses =
   let
-    val axclauses = map snd (make_axiom_clauses thy axcls)
     val ct = fold (fold count_fol_formula) [conjectures, axclauses]
                   init_counters
     fun is_needed c = the (Symtab.lookup ct c) > 0
@@ -280,7 +276,7 @@
                    if exists is_needed ss then map (`Thm.get_name_hint) ths
                    else [])) @
       (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
-  in map snd (make_axiom_clauses thy cnfs) end
+  in map (snd o make_axiom_clause thy) cnfs end
 
 fun s_not (@{const Not} $ t) = t
   | s_not t = @{const Not} $ t
@@ -298,10 +294,13 @@
     val tycons = type_consts_of_terms thy (goal_t :: axtms)
     (* TFrees in conjecture clauses; TVars in axiom clauses *)
     val conjectures = make_conjecture_clauses thy (map s_not hyp_ts @ [concl_t])
-    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
-    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
+    val extra_clauses = map (snd o make_axiom_clause thy) extra_cls
+    val (clnames, axiom_clauses) =
+      ListPair.unzip (map (make_axiom_clause thy) axcls)
+    (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
+       "get_helper_clauses" call? *)
     val helper_clauses =
-      get_helper_clauses thy is_FO full_types conjectures extra_cls
+      get_helper_clauses thy is_FO full_types conjectures extra_clauses
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in