src/HOL/Tools/inductive_package.ML
changeset 11628 e57a6e51715e
parent 11502 e80a712982e1
child 11682 d9063229b4a1
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:18:46 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:19:26 2001 +0200
     1.3 @@ -49,11 +49,11 @@
     1.4    val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
     1.5      -> theory -> theory
     1.6    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     1.7 -    theory attribute list -> ((bstring * term) * theory attribute list) list ->
     1.8 +    ((bstring * term) * theory attribute list) list ->
     1.9        thm list -> thm list -> theory -> theory *
    1.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.12 -  val add_inductive: bool -> bool -> string list -> Args.src list ->
    1.13 +  val add_inductive: bool -> bool -> string list ->
    1.14      ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    1.15        (xstring * Args.src list) list -> theory -> theory *
    1.16        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.17 @@ -741,7 +741,7 @@
    1.18    in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
    1.19  
    1.20  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    1.21 -    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.22 +    intros monos con_defs thy params paramTs cTs cnames induct_cases =
    1.23    let
    1.24      val _ =
    1.25        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    1.26 @@ -772,7 +772,7 @@
    1.27      val (thy3, ([intrs'', elims'], [induct'])) =
    1.28        thy2
    1.29        |> PureThy.add_thmss
    1.30 -        [(("intros", intrs'), atts),
    1.31 +        [(("intros", intrs'), []),
    1.32            (("elims", elims), [RuleCases.consumes 1])]
    1.33        |>>> PureThy.add_thms
    1.34          [((coind_prefix coind ^ "induct", rulify induct),
    1.35 @@ -799,7 +799,7 @@
    1.36    | None => error (msg ^ Sign.string_of_term sign t));
    1.37  
    1.38  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    1.39 -    atts pre_intros monos con_defs thy =
    1.40 +    pre_intros monos con_defs thy =
    1.41    let
    1.42      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
    1.43      val sign = Theory.sign_of thy;
    1.44 @@ -822,19 +822,18 @@
    1.45      val induct_cases = map (#1 o #1) intros;
    1.46  
    1.47      val (thy1, result as {elims, induct, ...}) =
    1.48 -      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
    1.49 +      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    1.50          con_defs thy params paramTs cTs cnames induct_cases;
    1.51      val thy2 = thy1
    1.52        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.53        |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
    1.54    in (thy2, result) end;
    1.55  
    1.56 -fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
    1.57 +fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
    1.58    let
    1.59      val sign = Theory.sign_of thy;
    1.60      val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
    1.61  
    1.62 -    val atts = map (Attrib.global_attribute thy) srcs;
    1.63      val intr_names = map (fst o fst) intro_srcs;
    1.64      fun read_rule s = Thm.read_cterm sign (s, propT)
    1.65        handle ERROR => error ("The error(s) above occurred for " ^ s);
    1.66 @@ -847,7 +846,7 @@
    1.67        |> apfst (IsarThy.apply_theorems raw_con_defs);
    1.68    in
    1.69      add_inductive_i verbose false "" coind false false cs'
    1.70 -      atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
    1.71 +      ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
    1.72    end;
    1.73  
    1.74  
    1.75 @@ -867,13 +866,13 @@
    1.76  
    1.77  local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.78  
    1.79 -fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
    1.80 -  #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
    1.81 +fun mk_ind coind (((sets, intrs), monos), con_defs) =
    1.82 +  #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
    1.83  
    1.84  fun ind_decl coind =
    1.85    (Scan.repeat1 P.term --| P.marg_comment) --
    1.86    (P.$$$ "intros" |--
    1.87 -    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
    1.88 +    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
    1.89    Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
    1.90    Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
    1.91    >> (Toplevel.theory o mk_ind coind);