src/HOL/Tools/inductive_package.ML
changeset 18787 5784fe1b5657
parent 18728 6790126ab5f6
child 18799 f137c5e971f5
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jan 25 00:21:44 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 26 15:37:14 2006 +0100
     1.3 @@ -500,7 +500,7 @@
     1.4    let
     1.5      val _ = clean_message "  Proving the elimination rules ...";
     1.6  
     1.7 -    val rules1 = [CollectE, disjE, make_elim vimageD, exE];
     1.8 +    val rules1 = [CollectE, disjE, make_elim vimageD, exE, FalseE];
     1.9      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    1.10    in
    1.11      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    1.12 @@ -657,7 +657,7 @@
    1.13           rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
    1.14           fold_goals_tac rec_sets_defs,
    1.15           (*This CollectE and disjE separates out the introduction rules*)
    1.16 -         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
    1.17 +         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE, FalseE])),
    1.18           (*Now break down the individual cases.  No disjE here in case
    1.19             some premise involves disjunction.*)
    1.20           REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
    1.21 @@ -719,7 +719,8 @@
    1.22      (* make a disjunction of all introduction rules *)
    1.23  
    1.24      val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
    1.25 -      absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
    1.26 +      absfree (xname, sumT, if null intr_ts then HOLogic.false_const
    1.27 +        else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
    1.28  
    1.29      (* add definiton of recursive sets to theory *)
    1.30  
    1.31 @@ -880,7 +881,7 @@
    1.32  fun ind_decl coind =
    1.33    Scan.repeat1 P.term --
    1.34    (P.$$$ "intros" |--
    1.35 -    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
    1.36 +    P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
    1.37    Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
    1.38    >> (Toplevel.theory o mk_ind coind);
    1.39