src/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 res_inst_tac ctxt [((xi, Position.none), s)] rule i st end
+  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), 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 = Logic.dest_conjunctions (Thm.concl_of rule);
     val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
       error "Induction rule has different numbers of variables";
-  in res_inst_tac ctxt insts rule' i st end
+  in Rule_Insts.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;