src/HOL/Tools/inductive_package.ML

--- a/src/HOL/Tools/inductive_package.ML	Mon Nov 05 18:18:39 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Nov 05 20:50:41 2007 +0100
@@ -725,6 +725,7 @@
 fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind}
     cs intros monos params cnames_syn ctxt =
   let
+    val _ = null cnames_syn andalso error "No inductive predicates given";
     val _ =
       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
         commas_quote (map fst cnames_syn)) else ();