src/HOL/Tools/res_axioms.ML

             val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                     (*Forms a lambda-abstraction over the formal parameters*)
             val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
             val cdef = cname ^ "_def"
             val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
-              handle ERROR _ => raise Clausify_failure thy'
             val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
           let val fname = Name.variant (add_term_names (p, [])) a

         val s = flatten_name name
         val (defs, thy') = declare_skofuns s nnfth thy
         val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
         val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
                          |> Meson.finish_cnf |> map Thm.close_derivation
-      in (cnfs', thy') end
-      handle Clausify_failure thy_e => ([], thy_e))   (* FIXME !? *)
+      in (cnfs', thy') end)
   end;
 
 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   Skolem functions.*)
 structure ThmCache = TheoryDataFun

 
 (**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
 (*Populate the clause cache using the supplied theorem. Return the clausal form
   and modified theory.*)
-fun skolem_cache_thm (name, th) thy =
+fun skolem_cache_thm name (i, th) thy =
   if bad_for_atp th then thy
   else
     (case lookup_cache thy th of
       SOME _ => thy
     | NONE =>
-        (case skolem (name, th) thy of
+        (case skolem (name ^ "_" ^ string_of_int (i + 1), th) thy of
           NONE => thy
         | SOME (cls, thy') => update_cache (th, cls) thy'));
 
 fun skolem_cache_fact (name, ths) (changed, thy) =
   if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name
   then (changed, thy)
-  else (true, thy |> mark_seen name |> fold skolem_cache_thm (PureThy.name_multi name ths));
+  else (true, thy |> mark_seen name |> fold_index (skolem_cache_thm name) ths);
 
 fun saturate_skolem_cache thy =
   (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of
     (false, _) => NONE
   | (true, thy') => SOME thy');