improved error msg;
authorwenzelm
Sat Jul 22 12:58:12 2000 +0200 (2000-07-22)
changeset 94053235873fdd90
parent 9404 99476cf93dad
child 9406 d505b11ce30d
improved error msg;
thm foo.cases;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 21 18:11:54 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jul 22 12:58:12 2000 +0200
     1.3 @@ -384,13 +384,17 @@
     1.4  
     1.5  fun add_cases_induct no_elim no_ind names elims induct induct_cases =
     1.6    let
     1.7 -    fun cases_spec (name, elim) = (("", elim), [InductMethod.cases_set_global name]);
     1.8 +    fun cases_spec (name, elim) thy =
     1.9 +      thy
    1.10 +      |> Theory.add_path (Sign.base_name name)
    1.11 +      |> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])])
    1.12 +      |> Theory.parent_path;
    1.13      val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    1.14  
    1.15 -    fun induct_spec (name, th) =
    1.16 -      (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
    1.17 +    fun induct_spec (name, th) = (#1 o PureThy.add_thms
    1.18 +      [(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]);
    1.19      val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
    1.20 -  in #1 o PureThy.add_thms (cases_specs @ induct_specs) end;
    1.21 +  in Library.apply (cases_specs @ induct_specs) end;
    1.22  
    1.23  
    1.24  
    1.25 @@ -782,14 +786,13 @@
    1.26      val _ = seq (check_rule sign cs o snd o fst) intros;
    1.27      val induct_cases = map (#1 o #1) intros;
    1.28  
    1.29 -    val (thy1, result) =
    1.30 +    val (thy1, result as {elims, induct, ...}) =
    1.31        (if ! quick_and_dirty then add_ind_axm else add_ind_def)
    1.32          verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    1.33          con_defs thy params paramTs cTs cnames induct_cases;
    1.34      val thy2 = thy1
    1.35        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.36 -      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames
    1.37 -          (#elims result) (#induct result) induct_cases;
    1.38 +      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
    1.39    in (thy2, result) end;
    1.40  
    1.41  
    1.42 @@ -803,7 +806,9 @@
    1.43  
    1.44      val atts = map (Attrib.global_attribute thy) srcs;
    1.45      val intr_names = map (fst o fst) intro_srcs;
    1.46 -    val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
    1.47 +    fun read_rule s = Thm.read_cterm sign (s, propT)
    1.48 +      handle ERROR => error ("The error(s) above occurred for " ^ s);
    1.49 +    val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
    1.50      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    1.51      val (cs', intr_ts') = unify_consts sign cs intr_ts;
    1.52