--- a/src/Tools/induct_tacs.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Tools/induct_tacs.ML Fri Mar 20 14:48:04 2015 +0100
@@ -44,7 +44,7 @@
(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;
@@ -104,7 +104,7 @@
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;