# HG changeset patch
# User wenzelm
# Date 1194292241 -3600
# Node ID 6e0c8dd213df9a8b85f3a1473e7e063cf7b1661c
# Parent  094dab519ff58a958b3b6ab5c368660306cd7fd3
improved error message for missing predicates;

diff -r 094dab519ff5 -r 6e0c8dd213df 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 ();