src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 57707 0242e9578828
parent 57703 fefe3ea75289
child 57709 9cda0c64c37a
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -498,7 +498,7 @@
 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
 
 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
-  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then
+  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
    else
      I)