# HG changeset patch
# User wenzelm
# Date 1214240424 -7200
# Node ID 1f0ac20db386640098ed93c2d4bd45bcf21e8b32
# Parent  efd626efcb0482f2bbe202ca0c72999bb3187d03
induct_tac: allow omission of arguments;

diff -r efd626efcb04 -r 1f0ac20db386 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)