src/HOL/simpdata.ML
changeset 18529 540da2415751
parent 18407 fa075b606571
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
     1.3 @@ -433,8 +433,7 @@
     1.4  structure Clasimp = ClasimpFun
     1.5   (structure Simplifier = Simplifier and Splitter = Splitter
     1.6    and Classical  = Classical and Blast = Blast
     1.7 -  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
     1.8 -  val cla_make_elim = cla_make_elim);
     1.9 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
    1.10  open Clasimp;
    1.11  
    1.12  val HOL_css = (HOL_cs, HOL_ss);