src/HOL/Tools/simpdata.ML
changeset 42478 8a526c010c3b
parent 42460 1805c67dc7aa
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:27:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:49:39 2011 +0200
     1.3 @@ -151,10 +151,16 @@
     1.4  
     1.5  (* integration of simplifier with classical reasoner *)
     1.6  
     1.7 -structure Clasimp = ClasimpFun
     1.8 - (structure Simplifier = Simplifier and Splitter = Splitter
     1.9 -  and Classical  = Classical and Blast = Blast
    1.10 -  val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
    1.11 +structure Clasimp = Clasimp
    1.12 +(
    1.13 +  structure Simplifier = Simplifier
    1.14 +    and Splitter = Splitter
    1.15 +    and Classical  = Classical
    1.16 +    and Blast = Blast
    1.17 +  val iffD1 = @{thm iffD1}
    1.18 +  val iffD2 = @{thm iffD2}
    1.19 +  val notE = @{thm notE}
    1.20 +);
    1.21  open Clasimp;
    1.22  
    1.23  val _ = ML_Antiquote.value "clasimpset"