diff -r 85e7f80023fc -r 540da2415751 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat Dec 31 21:49:35 2005 +0100
+++ b/src/FOL/simpdata.ML	Sat Dec 31 21:49:36 2005 +0100
@@ -369,8 +369,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Cla and Blast = Blast
-  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
-  val cla_make_elim = cla_make_elim);
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);