# HG changeset patch
# User paulson
# Date 1140449018 -3600
# Node ID 2cb4559782f4733b40c1793f6683f076ac55a331
# Parent  f81f8706cd376829ba31c33d74a86874ed4363b8
Inclusion of subset_refl in ATP calls

diff -r f81f8706cd37 -r 2cb4559782f4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Feb 20 16:22:52 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Mon Feb 20 16:23:38 2006 +0100
@@ -346,7 +346,9 @@
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
-      val intros = safeIs @ hazIs
+      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 elims  = map Classical.classical_rule (safeEs @ hazEs)
   in
      Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^