src/HOL/Tools/induct_tacs.ML

 
     val xi =
       (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
         Var (xi, _) :: _ => xi
       | _ => raise THM ("Malformed cases rule", 0, [rule]));
-  in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end
+  in res_inst_tac ctxt [(xi, s)] rule i st end
   handle THM _ => Seq.empty;
 
 fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
 fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
 

     val _ = Method.trace ctxt [rule];
 
     val concls = HOLogic.dest_concls (Thm.concl_of rule);
     val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
       error "Induction rule has different numbers of variables";
-  in RuleInsts.res_inst_tac ctxt insts rule i st end
+  in res_inst_tac ctxt insts rule i st end
   handle THM _ => Seq.empty;
 
 end;
 
 fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);