src/HOL/Tools/res_axioms.ML

 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 (*also works for HOL*) 
 fun skolem_thm th = 
   let val nnfth = to_nnf th
-  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
+  in  rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
   end
   handle THM _ => [];
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)

   let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
   in Option.map 
         (fn nnfth => 
           let val (thy',defs) = declare_skofuns cname nnfth thy
               val skoths = map skolem_of_def defs
-          in (thy', Meson.make_cnf skoths nnfth) end)
+          in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)
       (SOME (to_nnf th)  handle THM _ => NONE) 
   end;
 
 (*Populate the clause cache using the supplied theorem. Return the clausal form
   and modified theory.*)

 val tag_intro = preserve_name (fn th => th RS tagI);
 val tag_elim  = preserve_name (fn th => tagD RS th);
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
-      val intros = [subset_refl] @ safeIs @ hazIs
-          (*subset_refl is a special case: obviously useful in resolution, but
-            harmful if added as a default intro rule.*)
+      val intros = safeIs @ hazIs
       val elims  = map Classical.classical_rule (safeEs @ hazEs)
   in
      Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ 
             " elims: " ^ Int.toString(length elims));
      if tagging_enabled