src/HOL/simpdata.ML
changeset 5220 07f80f447b27
parent 5219 924359415f09
child 5278 a903b66822e2
     1.1 --- a/src/HOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jul 30 19:18:50 1998 +0200
     1.3 @@ -474,8 +474,8 @@
     1.4  
     1.5  structure Clasimp = ClasimpFun
     1.6   (structure Simplifier = Simplifier and Classical = Classical 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