--- a/src/FOL/simpdata.ML Tue Apr 26 21:27:01 2011 +0200
+++ b/src/FOL/simpdata.ML Tue Apr 26 21:49:39 2011 +0200
@@ -130,10 +130,16 @@
(*** integration of simplifier with classical reasoner ***)
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Splitter = Splitter
- and Classical = Cla and Blast = Blast
- val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
+structure Clasimp = Clasimp
+(
+ structure Simplifier = Simplifier
+ and Splitter = Splitter
+ and Classical = Cla
+ and Blast = Blast
+ val iffD1 = @{thm iffD1}
+ val iffD2 = @{thm iffD2}
+ val notE = @{thm notE}
+);
open Clasimp;
ML_Antiquote.value "clasimpset"