src/FOL/simpdata.ML
changeset 11344 57b7ad51971c
parent 11232 558a4feebb04
child 11748 06eb315831ff
     1.1 --- a/src/FOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
     1.3 @@ -359,9 +359,7 @@
     1.4  structure Clasimp = ClasimpFun
     1.5   (structure Simplifier = Simplifier and Splitter = Splitter
     1.6    and Classical  = Cla and Blast = Blast
     1.7 -  val dest_Trueprop = FOLogic.dest_Trueprop
     1.8 -  val iff_const = FOLogic.iff val not_const = FOLogic.not
     1.9 -  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    1.10 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
    1.11    val cla_make_elim = cla_make_elim);
    1.12  open Clasimp;
    1.13