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