made SML/NJ happy;
authorwenzelm
Thu Jul 30 19:18:50 1998 +0200 (1998-07-30)
changeset 522007f80f447b27
parent 5219 924359415f09
child 5221 7e9f9ab61798
made SML/NJ happy;
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 30 19:18:50 1998 +0200
     1.3 @@ -352,8 +352,8 @@
     1.4  
     1.5  structure Clasimp = ClasimpFun
     1.6   (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
     1.7 -  val addcongs = op addcongs and delcongs = op delcongs
     1.8 -  and addSaltern = op addSaltern and addbefore = op addbefore);
     1.9 +  val op addcongs = op addcongs and op delcongs = op delcongs
    1.10 +  and op addSaltern = op addSaltern and op addbefore = op addbefore);
    1.11  
    1.12  open Clasimp;
    1.13  
     2.1 --- a/src/HOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Thu Jul 30 19:18:50 1998 +0200
     2.3 @@ -474,8 +474,8 @@
     2.4  
     2.5  structure Clasimp = ClasimpFun
     2.6   (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
     2.7 -  val addcongs = op addcongs and delcongs = op delcongs
     2.8 -  and addSaltern = op addSaltern and addbefore = op addbefore);
     2.9 +  val op addcongs = op addcongs and op delcongs = op delcongs
    2.10 +  and op addSaltern = op addSaltern and op addbefore = op addbefore);
    2.11  
    2.12  open Clasimp;
    2.13