src/HOL/simpdata.ML

 structure Splitter = SplitterFun(SplitterData);
 
 val split_tac        = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
 val split_asm_tac    = Splitter.split_asm_tac;
-val addsplits        = Splitter.addsplits;
-val delsplits        = Splitter.delsplits;
+val op addsplits     = Splitter.addsplits;
+val op delsplits     = Splitter.delsplits;
 val Addsplits        = Splitter.Addsplits;
 val Delsplits        = Splitter.Delsplits;
 
 (** 'if' congruence rules: neither included by default! *)