diff -r 924359415f09 -r 07f80f447b27 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
+++ b/src/HOL/simpdata.ML	Thu Jul 30 19:18:50 1998 +0200
@@ -474,8 +474,8 @@
 
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
-  val addcongs = op addcongs and delcongs = op delcongs
-  and addSaltern = op addSaltern and addbefore = op addbefore);
+  val op addcongs = op addcongs and op delcongs = op delcongs
+  and op addSaltern = op addSaltern and op addbefore = op addbefore);
 
 open Clasimp;