diff -r d5f1b482bfbf -r 57b7ad51971c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
+++ b/src/HOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
@@ -454,10 +454,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val dest_Trueprop = HOLogic.dest_Trueprop
-  val iff_const = HOLogic.eq_const HOLogic.boolT
-  val not_const = HOLogic.not_const
-  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
   val cla_make_elim = cla_make_elim);
 open Clasimp;