--- 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);