--- a/src/FOL/simpdata.ML Thu May 31 16:51:26 2001 +0200
+++ b/src/FOL/simpdata.ML Thu May 31 16:52:02 2001 +0200
@@ -359,9 +359,7 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
and Classical = Cla and Blast = Blast
- val dest_Trueprop = FOLogic.dest_Trueprop
- val iff_const = FOLogic.iff val not_const = FOLogic.not
- 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;