src/ZF/Tools/induct_tacs.ML

     val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) =
         (case Thm.prems_of rule of
              [] => error "induction is not available for this datatype"
            | major::_ => FOLogic.dest_Trueprop major)
   in
-    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
+    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] [] rule i
   end
   handle Find_tname msg =>
             if exh then (*try boolean case analysis instead*)
-                case_tac ctxt var i
+                case_tac ctxt var [] i
             else error msg) i state;
 
 val exhaust_tac = exhaust_induct_tac true;
 val induct_tac = exhaust_induct_tac false;