# HG changeset patch
# User wenzelm
# Date 901819130 -7200
# Node ID 07f80f447b27c7e38473f887301dddf175d46008
# Parent  924359415f095dcdd71ba9a37d2d7db7b028d5d9
made SML/NJ happy;

diff -r 924359415f09 -r 07f80f447b27 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 30 19:18:50 1998 +0200
@@ -352,8 +352,8 @@
 
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Classical = Cla 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;
 
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;