src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Tue Oct 17 10:20:43 2000 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 17 10:21:12 2000 +0200
@@ -307,8 +307,8 @@
   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;