Fixed bug (improper handling of flag no_ind).

--- a/src/HOL/Tools/inductive_package.ML	Wed Jul 01 18:43:40 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jul 01 19:03:54 1998 +0200
@@ -454,7 +454,7 @@
       else
         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
           rec_sets_defs thy';
-    val induct = if coind orelse length cs > 1 then raw_induct
+    val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
       else standard (raw_induct RSN (2, rev_mp));
 
     val thy'' = thy' |>