src/HOL/Tools/split_rule.ML

     val vars = collect_vars prop [];
   in
     fst (fold_rev complete_split_rule_var vars (rl, xs))
     |> remove_internal_split
     |> Drule.standard
-    |> RuleCases.save rl
+    |> Rule_Cases.save rl
   end;
 
 
 fun pair_tac ctxt s =
   res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}

   in
     rl
     |> fold_index one_goal xss
     |> Simplifier.full_simplify split_rule_ss
     |> Drule.standard
-    |> RuleCases.save rl
+    |> Rule_Cases.save rl
   end;
 
 
 (* attribute syntax *)