# HG changeset patch
# User wenzelm
# Date 1001697566 -7200
# Node ID e57a6e51715e4adeff3a1eaf32661163fbee2b27
# Parent  abf9cda4a4d20ef928f553f11d864201b4c2bea8
inductive: no collective atts;

diff -r abf9cda4a4d2 -r e57a6e51715e src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Fri Sep 28 19:19:26 2001 +0200
@@ -33,10 +33,10 @@
   "a |- e :: t" == "(a, e, t) : has_type"
 
 inductive has_type
-  intros [simp]
-    Var: "n < length a ==> a |- Var n :: a ! n"
-    Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
-    App: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
+  intros
+    Var [simp]: "n < length a ==> a |- Var n :: a ! n"
+    Abs [simp]: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
+    App [simp]: "a |- e1 :: t2 -> t1 ==> a |- e2 :: t2
       ==> a |- App e1 e2 :: t1"
 
 
diff -r abf9cda4a4d2 -r e57a6e51715e src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -182,7 +182,7 @@
     val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name' false false true
-           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
+           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
diff -r abf9cda4a4d2 -r e57a6e51715e src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -175,7 +175,7 @@
     val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name false true false
-           consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
+           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
 
     (********************************* typedef ********************************)
 
diff -r abf9cda4a4d2 -r e57a6e51715e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -49,11 +49,11 @@
   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
     -> theory -> theory
   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
-    theory attribute list -> ((bstring * term) * theory attribute list) list ->
+    ((bstring * term) * theory attribute list) list ->
       thm list -> thm list -> theory -> theory *
       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
-  val add_inductive: bool -> bool -> string list -> Args.src list ->
+  val add_inductive: bool -> bool -> string list ->
     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
       (xstring * Args.src list) list -> theory -> theory *
       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
@@ -741,7 +741,7 @@
   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
 
 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
-    atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
+    intros monos con_defs thy params paramTs cTs cnames induct_cases =
   let
     val _ =
       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
@@ -772,7 +772,7 @@
     val (thy3, ([intrs'', elims'], [induct'])) =
       thy2
       |> PureThy.add_thmss
-        [(("intros", intrs'), atts),
+        [(("intros", intrs'), []),
           (("elims", elims), [RuleCases.consumes 1])]
       |>>> PureThy.add_thms
         [((coind_prefix coind ^ "induct", rulify induct),
@@ -799,7 +799,7 @@
   | None => error (msg ^ Sign.string_of_term sign t));
 
 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
-    atts pre_intros monos con_defs thy =
+    pre_intros monos con_defs thy =
   let
     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
     val sign = Theory.sign_of thy;
@@ -822,19 +822,18 @@
     val induct_cases = map (#1 o #1) intros;
 
     val (thy1, result as {elims, induct, ...}) =
-      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
+      add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
         con_defs thy params paramTs cTs cnames induct_cases;
     val thy2 = thy1
       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
   in (thy2, result) end;
 
-fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
+fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
   let
     val sign = Theory.sign_of thy;
     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
 
-    val atts = map (Attrib.global_attribute thy) srcs;
     val intr_names = map (fst o fst) intro_srcs;
     fun read_rule s = Thm.read_cterm sign (s, propT)
       handle ERROR => error ("The error(s) above occurred for " ^ s);
@@ -847,7 +846,7 @@
       |> apfst (IsarThy.apply_theorems raw_con_defs);
   in
     add_inductive_i verbose false "" coind false false cs'
-      atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
+      ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   end;
 
 
@@ -867,13 +866,13 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
-  #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
+fun mk_ind coind (((sets, intrs), monos), con_defs) =
+  #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
 
 fun ind_decl coind =
   (Scan.repeat1 P.term --| P.marg_comment) --
   (P.$$$ "intros" |--
-    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
+    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   >> (Toplevel.theory o mk_ind coind);
diff -r abf9cda4a4d2 -r e57a6e51715e src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/thy_syntax.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -63,7 +63,7 @@
         \local\n\
         \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
         \  InductivePackage.add_inductive true " ^
-        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
+        (if coind then "true " else "false ") ^ srec_tms ^
          sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
         \in\n\
         \structure " ^ big_rec_name ^ " =\n\