src/Tools/induct_tacs.ML

--- a/src/Tools/induct_tacs.ML	Mon Jun 23 16:01:03 2008 +0200
+++ b/src/Tools/induct_tacs.ML	Mon Jun 23 19:00:24 2008 +0200
@@ -85,8 +85,6 @@
       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)