src/HOL/Tools/ATP/atp_proof_reconstruct.ML

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 21:52:44 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -28,6 +28,9 @@
   val partial_type_encs : string list
   val default_metis_lam_trans : string
 
+  val leo2_extcnf_equal_neg_rule : string
+  val satallax_tab_rule_prefix : string
+
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
   val simplify_bool : term -> term
@@ -91,6 +94,9 @@
 
 val default_metis_lam_trans = combsN
 
+val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
+val satallax_tab_rule_prefix = "tab_"
+
 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
   | term_name' _ = ""
 
@@ -499,10 +505,9 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
-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] rule then
+  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
+      String.isPrefix satallax_tab_rule_prefix rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
    else
      I)