src/HOL/simpdata.ML

   val meta_eq_to_iff = meta_eq_to_obj_eq
   val iffD           = iffD2
   val disjE          = disjE
   val conjE          = conjE
   val exE            = exE
-  val contrapos      = contrapos
-  val contrapos2     = contrapos2
+  val contrapos      = contrapos_nn
+  val contrapos2     = contrapos_pp
   val notnotD        = notnotD
   end;
 
 structure Splitter = SplitterFun(SplitterData);