src/HOL/Tools/inductive_set.ML

       set_arities = set_arities1, pred_arities = pred_arities1},
      {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
       set_arities = set_arities2, pred_arities = pred_arities2}) : T =
     {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
      to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
-     set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
-     pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
+     set_arities = Symtab.merge_list (op =) (set_arities1, set_arities2),
+     pred_arities = Symtab.merge_list (op =) (pred_arities1, pred_arities2)};
 );
 
 fun name_type_of (Free p) = SOME p
   | name_type_of (Const p) = SOME p
   | name_type_of _ = NONE;