src/Tools/induct_tacs.ML

       in #1 (check_type ctxt t) end;
 
     val argss = map (map (Option.map induct_var)) varss;
     val rule =
       (case opt_rules of
-        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
+        SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
       | NONE =>
-          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
+          (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
             (_, rule) :: _ => rule
           | [] => raise THM ("No induction rules", 0, [])));
 
     val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
     val _ = Method.trace ctxt [rule'];