# HG changeset patch
# User berghofe
# Date 1138286234 -3600
# Node ID 5784fe1b5657b42f635c9152f324ec10c8416598
# Parent  591a37d48794b4c60045d7a1b9d27df9eca03f8d
Inductive sets with no introduction rules are now allowed as well.

diff -r 591a37d48794 -r 5784fe1b5657 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jan 25 00:21:44 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 26 15:37:14 2006 +0100
@@ -500,7 +500,7 @@
   let
     val _ = clean_message "  Proving the elimination rules ...";
 
-    val rules1 = [CollectE, disjE, make_elim vimageD, exE];
+    val rules1 = [CollectE, disjE, make_elim vimageD, exE, FalseE];
     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   in
     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
@@ -657,7 +657,7 @@
          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
          fold_goals_tac rec_sets_defs,
          (*This CollectE and disjE separates out the introduction rules*)
-         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
+         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
@@ -719,7 +719,8 @@
     (* make a disjunction of all introduction rules *)
 
     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
-      absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
+      absfree (xname, sumT, if null intr_ts then HOLogic.false_const
+        else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
 
     (* add definiton of recursive sets to theory *)
 
@@ -880,7 +881,7 @@
 fun ind_decl coind =
   Scan.repeat1 P.term --
   (P.$$$ "intros" |--
-    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
+    P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
   >> (Toplevel.theory o mk_ind coind);