src/HOL/simpdata.ML

 end;
 
 
 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;
 
 val HOL_css = (HOL_cs, HOL_ss);