diff -r 3ee568334813 -r 35eeb95c5bee src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 09:19:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 09:26:56 2010 +0200
@@ -142,24 +142,23 @@
 fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
+fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
   let
-    val (skolem_somes, t) =
-      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
+    val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems
     val (lits, ctypes_sorts) = literals_of_term thy t
   in
     if forall is_false_literal lits then
       raise TRIVIAL ()
     else
-      (skolem_somes,
+      (skolems,
        HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   end
 
-fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) =
+fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
   let
-    val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes
-  in (skolem_somes, clss |> not (is_tautology cls) ? cons (name, cls)) end
+    val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
+  in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end
 
 fun make_axiom_clauses thy clauses =
   ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
@@ -167,11 +166,11 @@
 fun make_conjecture_clauses thy =
   let
     fun aux _ _ [] = []
-      | aux n skolem_somes (th :: ths) =
+      | aux n skolems (th :: ths) =
         let
-          val (skolem_somes, cls) =
-            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
-        in cls :: aux (n + 1) skolem_somes ths end
+          val (skolems, cls) =
+            make_clause thy (n, "conjecture", Conjecture, th) skolems
+        in cls :: aux (n + 1) skolems ths end
   in aux 0 [] end
 
 (** Helper clauses **)