src/Tools/induct_tacs.ML

             warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
           else ();
       in #1 (check_type ctxt t) end;
 
     val argss = map (map (Option.map induct_var)) varss;
-    val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
-
     val rule =
       (case opt_rules of
         SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
       | NONE =>
           (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of