src/HOL/Tools/SMT/verit_replay_methods.ML

   | verit_rule_of "trans" = Trans
   | verit_rule_of "false" = False
   | verit_rule_of "ac_simp" = AC_Simp
   | verit_rule_of "and" = And
   | verit_rule_of "not_and" = Not_And
-  | verit_rule_of "and_pos" = And_Pos
   | verit_rule_of "and_neg" = And_Neg
   | verit_rule_of "or_pos" = Or_Pos
   | verit_rule_of "or_neg" = Or_Neg
   | verit_rule_of "not_equiv1" = Not_Equiv1
   | verit_rule_of "not_equiv2" = Not_Equiv2

      else if r = Lethe_Proof.eq_congruent_rule then Eq_Congruent
      else if r = Lethe_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
      else if r = Lethe_Proof.theory_resolution2_rule then Theory_Resolution2
      else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution
      else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2
+     else if r = Lethe_Proof.and_pos_rule then And_Pos
      else (@{print} ("Unsupport rule", r); Unsupported)
 
 
 (* Combining all together *)