simplified type attribute;
authorwenzelm
Sat Jan 21 23:02:14 2006 +0100 (2006-01-21)
changeset 187286790126ab5f6
parent 18727 caf9bc780c80
child 18729 216e31270509
simplified type attribute;
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/typedef_package.ML
src/HOL/arith_data.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/HOLCF/pcpodef_package.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/args.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
src/Pure/Tools/class_package.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/pure_thy.ML
src/Pure/simplifier.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -258,15 +258,16 @@
     1.4  val hol4_debug = ref false
     1.5  fun message s = if !hol4_debug then writeln s else ()
     1.6  
     1.7 -fun add_hol4_rewrite (thy,th) =
     1.8 +fun add_hol4_rewrite (context, th) =
     1.9      let
    1.10 +        val thy = Context.the_theory context;
    1.11  	val _ = message "Adding HOL4 rewrite"
    1.12  	val th1 = th RS eq_reflection
    1.13  	val current_rews = HOL4Rewrites.get thy
    1.14  	val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
    1.15  	val updated_thy  = HOL4Rewrites.put new_rews thy
    1.16      in
    1.17 -	(updated_thy,th1)
    1.18 +	(Context.Theory updated_thy,th1)
    1.19      end;
    1.20  
    1.21  fun ignore_hol4 bthy bthm thy =
    1.22 @@ -775,8 +776,5 @@
    1.23    ImportSegment.init #>
    1.24    initial_maps #>
    1.25    Attrib.add_attributes
    1.26 -    [("hol4rew",
    1.27 -      (Attrib.no_args add_hol4_rewrite,
    1.28 -       Attrib.no_args Attrib.undef_local_attribute),
    1.29 -      "HOL4 rewrite rule")]
    1.30 +    [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
    1.31  end
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jan 20 04:53:59 2006 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Jan 21 23:02:14 2006 +0100
     2.3 @@ -1988,7 +1988,7 @@
     2.4  	    val thy1 = foldr (fn(name,thy)=>
     2.5  				snd (get_defname thyname name thy)) thy1 names
     2.6  	    fun new_name name = fst (get_defname thyname name thy1)
     2.7 -	    val (thy',res) = SpecificationPackage.add_specification_i NONE
     2.8 +	    val (thy',res) = SpecificationPackage.add_specification NONE
     2.9  				 (map (fn name => (new_name name,name,false)) names)
    2.10  				 (thy1,th)
    2.11  	    val res' = Drule.freeze_all res
     3.1 --- a/src/HOL/Import/shuffler.ML	Fri Jan 20 04:53:59 2006 +0100
     3.2 +++ b/src/HOL/Import/shuffler.ML	Sat Jan 21 23:02:14 2006 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4      val print_shuffles: theory -> unit
     3.5  
     3.6      val add_shuffle_rule: thm -> theory -> theory
     3.7 -    val shuffle_attr: theory attribute
     3.8 +    val shuffle_attr: attribute
     3.9  
    3.10      val setup      : theory -> theory
    3.11  end
    3.12 @@ -682,7 +682,7 @@
    3.13  	else ShuffleData.put (thm::shuffles) thy
    3.14      end
    3.15  
    3.16 -fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm)
    3.17 +val shuffle_attr = Thm.declaration_attribute (Context.map_theory o add_shuffle_rule);
    3.18  
    3.19  val setup =
    3.20    Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
    3.21 @@ -693,6 +693,6 @@
    3.22    add_shuffle_rule imp_comm #>
    3.23    add_shuffle_rule Drule.norm_hhf_eq #>
    3.24    add_shuffle_rule Drule.triv_forall_equality #>
    3.25 -  Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]
    3.26 +  Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
    3.27  
    3.28  end
     4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jan 20 04:53:59 2006 +0100
     4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jan 21 23:02:14 2006 +0100
     4.3 @@ -19,7 +19,7 @@
     4.4  sig
     4.5    val prove_casedist_thms : string list ->
     4.6      DatatypeAux.descr list -> (string * sort) list -> thm ->
     4.7 -    theory attribute list -> theory -> thm list * theory
     4.8 +    attribute list -> theory -> thm list * theory
     4.9    val prove_primrec_thms : bool -> string list ->
    4.10      DatatypeAux.descr list -> (string * sort) list ->
    4.11        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
     5.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Jan 20 04:53:59 2006 +0100
     5.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sat Jan 21 23:02:14 2006 +0100
     5.3 @@ -15,10 +15,10 @@
     5.4    val add_path : bool -> string -> theory -> theory
     5.5    val parent_path : bool -> theory -> theory
     5.6  
     5.7 -  val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
     5.8 +  val store_thmss_atts : string -> string list -> attribute list list -> thm list list
     5.9      -> theory -> thm list list * theory
    5.10    val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    5.11 -  val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    5.12 +  val store_thms_atts : string -> string list -> attribute list list -> thm list
    5.13      -> theory -> thm list * theory
    5.14    val store_thms : string -> string list -> thm list -> theory -> thm list * theory
    5.15  
     6.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 20 04:53:59 2006 +0100
     6.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 21 23:02:14 2006 +0100
     6.3 @@ -39,8 +39,8 @@
     6.4         induction : thm,
     6.5         size : thm list,
     6.6         simps : thm list} * theory
     6.7 -  val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
     6.8 -    (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
     6.9 +  val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
    6.10 +    (thm list * attribute list) list list -> (thm list * attribute list) ->
    6.11      theory ->
    6.12        {distinct : thm list list,
    6.13         inject : thm list list,
    6.14 @@ -350,10 +350,10 @@
    6.15                    weak_case_congs cong_att =
    6.16    (snd o PureThy.add_thmss [(("simps", simps), []),
    6.17      (("", List.concat case_thms @ size_thms @ 
    6.18 -          List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
    6.19 +          List.concat distinct  @ rec_thms), [Simplifier.simp_add]),
    6.20      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    6.21 -    (("", List.concat inject),               [Attrib.theory iff_add]),
    6.22 -    (("", map name_notE (List.concat distinct)),  [Attrib.theory (Classical.safe_elim NONE)]),
    6.23 +    (("", List.concat inject),               [iff_add]),
    6.24 +    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim NONE]),
    6.25      (("", weak_case_congs),                  [cong_att])]);
    6.26  
    6.27  
    6.28 @@ -365,10 +365,10 @@
    6.29      fun proj i = ProjectRule.project induction (i + 1);
    6.30  
    6.31      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    6.32 -      [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]),
    6.33 -       (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])];
    6.34 +      [(("", proj index), [InductAttrib.induct_type name]),
    6.35 +       (("", exhaustion), [InductAttrib.cases_type name])];
    6.36      fun unnamed_rule i =
    6.37 -      (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]);
    6.38 +      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
    6.39    in
    6.40      PureThy.add_thms
    6.41        (List.concat (map named_rules infos) @
    6.42 @@ -747,7 +747,7 @@
    6.43        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
    6.44        |> Theory.add_path (space_implode "_" new_type_names)
    6.45        |> add_rules simps case_thms size_thms rec_thms inject distinct
    6.46 -           weak_case_congs (Attrib.theory Simplifier.cong_add)
    6.47 +          weak_case_congs Simplifier.cong_add
    6.48        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    6.49        |> add_cases_induct dt_infos induct
    6.50        |> Theory.parent_path
    6.51 @@ -806,7 +806,7 @@
    6.52        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
    6.53        |> Theory.add_path (space_implode "_" new_type_names)
    6.54        |> add_rules simps case_thms size_thms rec_thms inject distinct
    6.55 -            weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
    6.56 +          weak_case_congs (Simplifier.attrib (op addcongs))
    6.57        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    6.58        |> add_cases_induct dt_infos induct
    6.59        |> Theory.parent_path
    6.60 @@ -913,7 +913,7 @@
    6.61      val thy11 = thy10 |>
    6.62        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    6.63        add_rules simps case_thms size_thms rec_thms inject distinct
    6.64 -                weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |> 
    6.65 +        weak_case_congs (Simplifier.attrib (op addcongs)) |> 
    6.66        put_datatypes (fold Symtab.update dt_infos dt_info) |>
    6.67        add_cases_induct dt_infos induction' |>
    6.68        Theory.parent_path |>
     7.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jan 20 04:53:59 2006 +0100
     7.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 21 23:02:14 2006 +0100
     7.3 @@ -15,7 +15,7 @@
     7.4  sig
     7.5    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     7.6      string list -> DatatypeAux.descr list -> (string * sort) list ->
     7.7 -      (string * mixfix) list -> (string * mixfix) list list -> theory attribute
     7.8 +      (string * mixfix) list -> (string * mixfix) list list -> attribute
     7.9          -> theory -> (thm list list * thm list list * thm list list *
    7.10            DatatypeAux.simproc_dist list * thm) * theory
    7.11  end;
     8.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 20 04:53:59 2006 +0100
     8.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Jan 21 23:02:14 2006 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  
     8.5  signature INDUCTIVE_CODEGEN =
     8.6  sig
     8.7 -  val add : string option -> theory attribute
     8.8 +  val add : string option -> attribute
     8.9    val setup : theory -> theory
    8.10  end;
    8.11  
    8.12 @@ -45,7 +45,7 @@
    8.13  
    8.14  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    8.15  
    8.16 -fun add optmod (p as (thy, thm)) =
    8.17 +fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
    8.18    let
    8.19      val {intros, graph, eqns} = CodegenData.get thy;
    8.20      fun thyname_of s = (case optmod of
    8.21 @@ -54,22 +54,22 @@
    8.22        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    8.23          Const (s, _) =>
    8.24            let val cs = foldr add_term_consts [] (prems_of thm)
    8.25 -          in (CodegenData.put
    8.26 +          in CodegenData.put
    8.27              {intros = intros |>
    8.28               Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]),
    8.29               graph = foldr (uncurry (Graph.add_edge o pair s))
    8.30                 (Library.foldl add_node (graph, s :: cs)) cs,
    8.31 -             eqns = eqns} thy, thm)
    8.32 +             eqns = eqns} thy
    8.33            end
    8.34 -      | _ => (warn thm; p))
    8.35 +      | _ => (warn thm; thy))
    8.36      | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
    8.37          Const (s, _) =>
    8.38 -          (CodegenData.put {intros = intros, graph = graph,
    8.39 +          CodegenData.put {intros = intros, graph = graph,
    8.40               eqns = eqns |> Symtab.update
    8.41 -               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
    8.42 -      | _ => (warn thm; p))
    8.43 -    | _ => (warn thm; p))
    8.44 -  end;
    8.45 +               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy
    8.46 +      | _ => (warn thm; thy))
    8.47 +    | _ => (warn thm; thy))
    8.48 +  end));
    8.49  
    8.50  fun get_clauses thy s =
    8.51    let val {intros, graph, ...} = CodegenData.get thy
     9.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 20 04:53:59 2006 +0100
     9.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jan 21 23:02:14 2006 +0100
     9.3 @@ -38,16 +38,16 @@
     9.4       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
     9.5    val the_mk_cases: theory -> string -> string -> thm
     9.6    val print_inductives: theory -> unit
     9.7 -  val mono_add_global: theory attribute
     9.8 -  val mono_del_global: theory attribute
     9.9 +  val mono_add: attribute
    9.10 +  val mono_del: attribute
    9.11    val get_monos: theory -> thm list
    9.12    val inductive_forall_name: string
    9.13    val inductive_forall_def: thm
    9.14    val rulify: thm -> thm
    9.15    val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    9.16 -  val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    9.17 +  val inductive_cases_i: ((bstring * attribute list) * term list) list -> theory -> theory
    9.18    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    9.19 -    ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    9.20 +    ((bstring * term) * attribute list) list -> thm list -> theory -> theory *
    9.21        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    9.22         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    9.23    val add_inductive: bool -> bool -> string list ->
    9.24 @@ -128,7 +128,7 @@
    9.25  (** monotonicity rules **)
    9.26  
    9.27  val get_monos = #2 o InductiveData.get;
    9.28 -fun map_monos f = InductiveData.map (Library.apsnd f);
    9.29 +val map_monos = Context.map_theory o InductiveData.map o Library.apsnd;
    9.30  
    9.31  fun mk_mono thm =
    9.32    let
    9.33 @@ -148,12 +148,8 @@
    9.34  
    9.35  (* attributes *)
    9.36  
    9.37 -fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
    9.38 -fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
    9.39 -
    9.40 -val mono_attr =
    9.41 - (Attrib.add_del_args mono_add_global mono_del_global,
    9.42 -  Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
    9.43 +val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono);
    9.44 +val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono);
    9.45  
    9.46  
    9.47  
    9.48 @@ -435,12 +431,11 @@
    9.49        thy
    9.50        |> Theory.parent_path
    9.51        |> Theory.add_path (Sign.base_name name)
    9.52 -      |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
    9.53 +      |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set name])] |> snd
    9.54        |> Theory.restore_naming thy;
    9.55      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    9.56  
    9.57 -    val induct_att =
    9.58 -      Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
    9.59 +    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
    9.60      val induct_specs =
    9.61        if no_induct then I
    9.62        else
    9.63 @@ -577,7 +572,7 @@
    9.64       ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
    9.65    in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    9.66  
    9.67 -val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    9.68 +val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
    9.69  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    9.70  
    9.71  
    9.72 @@ -852,7 +847,7 @@
    9.73      fun read_rule s = Thm.read_cterm thy (s, propT)
    9.74        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
    9.75      val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
    9.76 -    val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    9.77 +    val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs;
    9.78      val (cs', intr_ts') = unify_consts thy cs intr_ts;
    9.79  
    9.80      val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
    9.81 @@ -871,7 +866,8 @@
    9.82    InductiveData.init #>
    9.83    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
    9.84      "dynamic case analysis on sets")] #>
    9.85 -  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
    9.86 +  Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
    9.87 +    "declaration of monotonicity rule")];
    9.88  
    9.89  
    9.90  (* outer syntax *)
    10.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 20 04:53:59 2006 +0100
    10.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 21 23:02:14 2006 +0100
    10.3 @@ -467,7 +467,7 @@
    10.4      Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
    10.5    end
    10.6  
    10.7 -fun rlz_attrib arg (thy, thm) =
    10.8 +fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
    10.9    let
   10.10      fun err () = error "ind_realizer: bad rule";
   10.11      val sets =
   10.12 @@ -476,21 +476,19 @@
   10.13           | xs => map (set_of o fst o HOLogic.dest_imp) xs)
   10.14           handle TERM _ => err () | Empty => err ();
   10.15    in 
   10.16 -    (add_ind_realizers (hd sets) (case arg of
   10.17 +    add_ind_realizers (hd sets)
   10.18 +      (case arg of
   10.19          NONE => sets | SOME NONE => []
   10.20        | SOME (SOME sets') => sets \\ sets')
   10.21 -      thy, thm)
   10.22 -  end;
   10.23 +  end);
   10.24  
   10.25 -val rlz_attrib_global = Attrib.syntax
   10.26 +val ind_realizer = Attrib.syntax
   10.27   ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   10.28      Scan.option (Scan.lift (Args.colon) |--
   10.29 -      Scan.repeat1 Args.global_const))) >> rlz_attrib);
   10.30 +      Scan.repeat1 Args.const))) >> rlz_attrib);
   10.31  
   10.32  val setup =
   10.33 -  Attrib.add_attributes [("ind_realizer",
   10.34 -    (rlz_attrib_global, K Attrib.undef_local_attribute),
   10.35 -    "add realizers for inductive set")];
   10.36 +  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
   10.37  
   10.38  end;
   10.39  
    11.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jan 20 04:53:59 2006 +0100
    11.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 21 23:02:14 2006 +0100
    11.3 @@ -10,7 +10,7 @@
    11.4    val quiet_mode: bool ref
    11.5    val add_primrec: string -> ((bstring * string) * Attrib.src list) list
    11.6      -> theory -> theory * thm list
    11.7 -  val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
    11.8 +  val add_primrec_i: string -> ((bstring * term) * attribute list) list
    11.9      -> theory -> theory * thm list
   11.10  end;
   11.11  
   11.12 @@ -258,7 +258,7 @@
   11.13      val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
   11.14      val thy''' = thy''
   11.15        |> (snd o PureThy.add_thmss [(("simps", simps'),
   11.16 -           [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
   11.17 +          [Simplifier.simp_add, RecfunCodegen.add NONE])])
   11.18        |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
   11.19        |> Theory.parent_path
   11.20    in
   11.21 @@ -270,7 +270,7 @@
   11.22    let
   11.23      val sign = Theory.sign_of thy;
   11.24      val ((names, strings), srcss) = apfst split_list (split_list eqns);
   11.25 -    val atts = map (map (Attrib.global_attribute thy)) srcss;
   11.26 +    val atts = map (map (Attrib.attribute thy)) srcss;
   11.27      val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT))
   11.28        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
   11.29      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
    12.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 20 04:53:59 2006 +0100
    12.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Jan 21 23:02:14 2006 +0100
    12.3 @@ -11,24 +11,23 @@
    12.4    val print_recdefs: theory -> unit
    12.5    val get_recdef: theory -> string
    12.6      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
    12.7 -  val simp_add: Context.generic attribute
    12.8 -  val simp_del: Context.generic attribute
    12.9 -  val cong_add: Context.generic attribute
   12.10 -  val cong_del: Context.generic attribute
   12.11 -  val wf_add: Context.generic attribute
   12.12 -  val wf_del: Context.generic attribute
   12.13 +  val simp_add: attribute
   12.14 +  val simp_del: attribute
   12.15 +  val cong_add: attribute
   12.16 +  val cong_del: attribute
   12.17 +  val wf_add: attribute
   12.18 +  val wf_del: attribute
   12.19    val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
   12.20      Attrib.src option -> theory -> theory
   12.21        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   12.22 -  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
   12.23 +  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
   12.24      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   12.25    val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
   12.26      -> theory -> theory * {induct_rules: thm}
   12.27 -  val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
   12.28 +  val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
   12.29      -> theory -> theory * {induct_rules: thm}
   12.30    val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
   12.31 -  val recdef_tc_i: bstring * theory attribute list -> string -> int option
   12.32 -    -> theory -> Proof.state
   12.33 +  val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
   12.34    val setup: theory -> theory
   12.35  end;
   12.36  
   12.37 @@ -148,7 +147,7 @@
   12.38  fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
   12.39    | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
   12.40  
   12.41 -fun attrib f = Attrib.declaration (map_hints o f);
   12.42 +fun attrib f = Thm.declaration_attribute (map_hints o f);
   12.43  
   12.44  val simp_add = attrib (map_simps o Drule.add_rule);
   12.45  val simp_del = attrib (map_simps o Drule.del_rule);
   12.46 @@ -165,15 +164,15 @@
   12.47  val recdef_wfN = "recdef_wf";
   12.48  
   12.49  val recdef_modifiers =
   12.50 - [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
   12.51 -  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
   12.52 -  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   12.53 -  Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
   12.54 -  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
   12.55 -  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
   12.56 -  Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
   12.57 -  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
   12.58 -  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
   12.59 + [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
   12.60 +  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
   12.61 +  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
   12.62 +  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
   12.63 +  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
   12.64 +  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
   12.65 +  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
   12.66 +  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
   12.67 +  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
   12.68    Clasimp.clasimp_modifiers;
   12.69  
   12.70  
   12.71 @@ -223,8 +222,7 @@
   12.72          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
   12.73                 congs wfs name R eqs;
   12.74      val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
   12.75 -    val simp_att = if null tcs then
   12.76 -      [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
   12.77 +    val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else [];
   12.78  
   12.79      val ((simps' :: rules', [induct']), thy) =
   12.80        thy
   12.81 @@ -239,7 +237,7 @@
   12.82        |> Theory.parent_path;
   12.83    in (thy, result) end;
   12.84  
   12.85 -val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints;
   12.86 +val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
   12.87  fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
   12.88  
   12.89  
   12.90 @@ -284,7 +282,7 @@
   12.91          " in recdef definition of " ^ quote name);
   12.92    in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
   12.93  
   12.94 -val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
   12.95 +val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
   12.96  val recdef_tc_i = gen_recdef_tc (K I) (K I);
   12.97  
   12.98  
   12.99 @@ -297,12 +295,9 @@
  12.100    GlobalRecdefData.init #>
  12.101    LocalRecdefData.init #>
  12.102    Attrib.add_attributes
  12.103 -   [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
  12.104 -      "declaration of recdef simp rule"),
  12.105 -    (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
  12.106 -      "declaration of recdef cong rule"),
  12.107 -    (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
  12.108 -      "declaration of recdef wf rule")];
  12.109 +   [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
  12.110 +    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
  12.111 +    (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
  12.112  
  12.113  
  12.114  (* outer syntax *)
    13.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Jan 20 04:53:59 2006 +0100
    13.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sat Jan 21 23:02:14 2006 +0100
    13.3 @@ -7,8 +7,8 @@
    13.4  
    13.5  signature RECFUN_CODEGEN =
    13.6  sig
    13.7 -  val add: string option -> theory attribute
    13.8 -  val del: theory attribute
    13.9 +  val add: string option -> attribute
   13.10 +  val del: attribute
   13.11    val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
   13.12    val get_thm_equations: theory -> string * typ -> (thm list * typ) option
   13.13    val setup: theory -> theory
   13.14 @@ -38,25 +38,25 @@
   13.15  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
   13.16    string_of_thm thm);
   13.17  
   13.18 -fun add optmod (p as (thy, thm)) =
   13.19 +fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
   13.20    let
   13.21      val tab = CodegenData.get thy;
   13.22      val (s, _) = const_of (prop_of thm);
   13.23    in
   13.24      if Pattern.pattern (lhs_of thm) then
   13.25 -      (CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy, thm)
   13.26 -    else (warn thm; p)
   13.27 -  end handle TERM _ => (warn thm; p);
   13.28 +      CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy
   13.29 +    else (warn thm; thy)
   13.30 +  end handle TERM _ => (warn thm; thy)));
   13.31  
   13.32 -fun del (p as (thy, thm)) =
   13.33 +val del = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
   13.34    let
   13.35      val tab = CodegenData.get thy;
   13.36      val (s, _) = const_of (prop_of thm);
   13.37    in case Symtab.lookup tab s of
   13.38 -      NONE => p
   13.39 -    | SOME thms => (CodegenData.put (Symtab.update (s,
   13.40 -        gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
   13.41 -  end handle TERM _ => (warn thm; p);
   13.42 +      NONE => thy
   13.43 +    | SOME thms =>
   13.44 +        CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
   13.45 +  end handle TERM _ => (warn thm; thy)));
   13.46  
   13.47  fun del_redundant thy eqs [] = eqs
   13.48    | del_redundant thy eqs (eq :: eqs') =
    14.1 --- a/src/HOL/Tools/record_package.ML	Fri Jan 20 04:53:59 2006 +0100
    14.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jan 21 23:02:14 2006 +0100
    14.3 @@ -1215,8 +1215,8 @@
    14.4  (* attributes *)
    14.5  
    14.6  fun case_names_fields x = RuleCases.case_names ["fields"] x;
    14.7 -fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)];
    14.8 -fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
    14.9 +fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
   14.10 +fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
   14.11  
   14.12  (* tactics *)
   14.13  
   14.14 @@ -1993,8 +1993,8 @@
   14.15      val final_thy =
   14.16        thms_thy
   14.17        |> (snd oo PureThy.add_thmss)
   14.18 -          [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
   14.19 -           (("iffs",iffs), [Attrib.theory iff_add])]
   14.20 +          [(("simps", sel_upd_simps), [Simplifier.simp_add]),
   14.21 +           (("iffs",iffs), [iff_add])]
   14.22        |> put_record name (make_record_info args parent fields extension induct_scheme')
   14.23        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
   14.24        |> add_record_equalities extension_id equality'
    15.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Jan 20 04:53:59 2006 +0100
    15.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat Jan 21 23:02:14 2006 +0100
    15.3 @@ -484,18 +484,15 @@
    15.4  (*Conjoin a list of clauses to recreate a single theorem*)
    15.5  val conj_rule = foldr1 conj2_rule;
    15.6  
    15.7 -fun skolem_global_fun (thy, th) = 
    15.8 -  let val name = Thm.name_of_thm th
    15.9 -      val (cls,thy') = skolem_cache_thm ((name,th), thy)
   15.10 -  in  (thy', conj_rule cls)  end;
   15.11 -
   15.12 -val skolem_global = Attrib.no_args skolem_global_fun;
   15.13 -
   15.14 -fun skolem_local x = Attrib.no_args (Attrib.rule (K (conj_rule o skolem_thm))) x;
   15.15 +fun skolem (Context.Theory thy, th) =
   15.16 +      let
   15.17 +        val name = Thm.name_of_thm th
   15.18 +        val (cls, thy') = skolem_cache_thm ((name, th), thy)
   15.19 +      in (Context.Theory thy', conj_rule cls) end
   15.20 +  | skolem (context, th) = (context, conj_rule (skolem_thm th));
   15.21  
   15.22  val setup_attrs = Attrib.add_attributes
   15.23 - [("skolem", (skolem_global, skolem_local),
   15.24 -    "skolemization of a theorem")];
   15.25 +  [("skolem", Attrib.no_args skolem, "skolemization of a theorem")];
   15.26  
   15.27  val setup = clause_cache_setup #> setup_attrs;
   15.28  
    16.1 --- a/src/HOL/Tools/split_rule.ML	Fri Jan 20 04:53:59 2006 +0100
    16.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Jan 21 23:02:14 2006 +0100
    16.3 @@ -136,13 +136,13 @@
    16.4  
    16.5  fun split_format x = Attrib.syntax
    16.6    (Scan.lift (Args.parens (Args.$$$ "complete"))
    16.7 -    >> K (Attrib.rule (K complete_split_rule)) ||
    16.8 +    >> K (Thm.rule_attribute (K complete_split_rule)) ||
    16.9    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   16.10 -    >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
   16.11 +    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
   16.12  
   16.13  val setup =
   16.14    Attrib.add_attributes
   16.15 -    [("split_format", (split_format, split_format),
   16.16 +    [("split_format", split_format,
   16.17        "split pair-typed subterms in premises, or function arguments")];
   16.18  
   16.19  end;
    17.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jan 20 04:53:59 2006 +0100
    17.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Jan 21 23:02:14 2006 +0100
    17.3 @@ -150,8 +150,8 @@
    17.4        else
    17.5          (NONE, thy);
    17.6  
    17.7 -    fun typedef_result (theory, nonempty) =
    17.8 -      theory
    17.9 +    fun typedef_result (context, nonempty) =
   17.10 +      Context.the_theory context
   17.11        |> put_typedef newT oldT (full Abs_name) (full Rep_name)
   17.12        |> add_typedecls [(t, vs, mx)]
   17.13        |> Theory.add_consts_i
   17.14 @@ -176,23 +176,19 @@
   17.15                  ((Rep_name ^ "_inject", make Rep_inject), []),
   17.16                  ((Abs_name ^ "_inject", make Abs_inject), []),
   17.17                  ((Rep_name ^ "_cases", make Rep_cases),
   17.18 -                  [RuleCases.case_names [Rep_name],
   17.19 -                    Attrib.theory (InductAttrib.cases_set full_name)]),
   17.20 +                  [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]),
   17.21                  ((Abs_name ^ "_cases", make Abs_cases),
   17.22 -                  [RuleCases.case_names [Abs_name],
   17.23 -                    Attrib.theory (InductAttrib.cases_type full_tname)]),
   17.24 +                  [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]),
   17.25                  ((Rep_name ^ "_induct", make Rep_induct),
   17.26 -                  [RuleCases.case_names [Rep_name],
   17.27 -                    Attrib.theory (InductAttrib.induct_set full_name)]),
   17.28 +                  [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
   17.29                  ((Abs_name ^ "_induct", make Abs_induct),
   17.30 -                  [RuleCases.case_names [Abs_name],
   17.31 -                    Attrib.theory (InductAttrib.induct_type full_tname)])])
   17.32 +                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])])
   17.33              ||> Theory.parent_path;
   17.34            val result = {type_definition = type_definition, set_def = set_def,
   17.35              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
   17.36              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
   17.37              Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
   17.38 -        in ((theory'', type_definition), result) end);
   17.39 +        in ((Context.Theory theory'', type_definition), result) end);
   17.40  
   17.41  
   17.42      (* errors *)
   17.43 @@ -220,7 +216,7 @@
   17.44  
   17.45      (*test theory errors now!*)
   17.46      val test_thy = Theory.copy thy;
   17.47 -    val _ = (test_thy,
   17.48 +    val _ = (Context.Theory test_thy,
   17.49        setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
   17.50  
   17.51    in (cset, goal, goal_pat, typedef_result) end
   17.52 @@ -239,7 +235,8 @@
   17.53      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
   17.54      val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
   17.55        cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   17.56 -    val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   17.57 +    val (thy', result) =
   17.58 +      (Context.Theory thy, non_empty) |> typedef_result |>> (Context.the_theory o fst);
   17.59    in (thy', result) end;
   17.60  
   17.61  in
    18.1 --- a/src/HOL/arith_data.ML	Fri Jan 20 04:53:59 2006 +0100
    18.2 +++ b/src/HOL/arith_data.ML	Sat Jan 21 23:02:14 2006 +0100
    18.3 @@ -223,8 +223,9 @@
    18.4    fun print _ _ = ();
    18.5  end);
    18.6  
    18.7 -fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
    18.8 -  {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
    18.9 +val arith_split_add = Thm.declaration_attribute (fn thm =>
   18.10 +  Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   18.11 +    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger})));
   18.12  
   18.13  fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   18.14    {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
   18.15 @@ -584,7 +585,5 @@
   18.16    Method.add_methods
   18.17      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
   18.18        "decide linear arithmethic")] #>
   18.19 -  Attrib.add_attributes [("arith_split",
   18.20 -    (Attrib.no_args arith_split_add,
   18.21 -     Attrib.no_args Attrib.undef_local_attribute),
   18.22 +  Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
   18.23      "declaration of split rules for arithmetic procedure")];
    19.1 --- a/src/HOLCF/domain/theorems.ML	Fri Jan 20 04:53:59 2006 +0100
    19.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jan 21 23:02:14 2006 +0100
    19.3 @@ -368,7 +368,7 @@
    19.4  		("inverts" , inverts ),
    19.5  		("injects" , injects ),
    19.6  		("copy_rews", copy_rews)])))
    19.7 -       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
    19.8 +       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add])])
    19.9         |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   19.10                   pat_rews @ dist_les @ dist_eqs @ copy_rews)
   19.11  end; (* let *)
    20.1 --- a/src/HOLCF/fixrec_package.ML	Fri Jan 20 04:53:59 2006 +0100
    20.2 +++ b/src/HOLCF/fixrec_package.ML	Sat Jan 21 23:02:14 2006 +0100
    20.3 @@ -7,14 +7,10 @@
    20.4  
    20.5  signature FIXREC_PACKAGE =
    20.6  sig
    20.7 -  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list
    20.8 -    -> theory -> theory
    20.9 -  val add_fixrec_i: bool -> ((string * theory attribute list) * term) list list
   20.10 -    -> theory -> theory
   20.11 -  val add_fixpat: (string * Attrib.src list) * string list
   20.12 -    -> theory -> theory
   20.13 -  val add_fixpat_i: (string * theory attribute list) * term list
   20.14 -    -> theory -> theory
   20.15 +  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
   20.16 +  val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
   20.17 +  val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
   20.18 +  val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
   20.19  end;
   20.20  
   20.21  structure FixrecPackage: FIXREC_PACKAGE =
   20.22 @@ -250,7 +246,7 @@
   20.23        val (simp_thms, thy'') = PureThy.add_thms simps thy';
   20.24        
   20.25        val simp_names = map (fn name => name^"_simps") cnames;
   20.26 -      val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
   20.27 +      val simp_attribute = rpair [Simplifier.simp_add];
   20.28        val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
   20.29      in
   20.30        (snd o PureThy.add_thmss simps') thy''
   20.31 @@ -258,7 +254,7 @@
   20.32      else thy'
   20.33    end;
   20.34  
   20.35 -val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.global_attribute;
   20.36 +val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
   20.37  val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
   20.38  
   20.39  
   20.40 @@ -286,7 +282,7 @@
   20.41      (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   20.42    end;
   20.43  
   20.44 -val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
   20.45 +val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
   20.46  val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
   20.47  
   20.48  
    21.1 --- a/src/HOLCF/pcpodef_package.ML	Fri Jan 20 04:53:59 2006 +0100
    21.2 +++ b/src/HOLCF/pcpodef_package.ML	Sat Jan 21 23:02:14 2006 +0100
    21.3 @@ -144,8 +144,9 @@
    21.4            ||> Theory.parent_path;
    21.5        in (theory', defs) end;
    21.6      
    21.7 -    fun pcpodef_result (theory, UUmem_admissible) =
    21.8 +    fun pcpodef_result (context, UUmem_admissible) =
    21.9        let
   21.10 +        val theory = Context.the_theory context;
   21.11          val UUmem = UUmem_admissible RS conjunct1;
   21.12          val admissible = UUmem_admissible RS conjunct2;
   21.13        in
   21.14 @@ -153,18 +154,19 @@
   21.15          |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
   21.16          |> make_cpo admissible
   21.17          |> make_pcpo UUmem
   21.18 -        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
   21.19 +        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
   21.20        end;
   21.21    
   21.22 -    fun cpodef_result (theory, nonempty_admissible) =
   21.23 +    fun cpodef_result (context, nonempty_admissible) =
   21.24        let
   21.25 +        val theory = Context.the_theory context;
   21.26          val nonempty = nonempty_admissible RS conjunct1;
   21.27          val admissible = nonempty_admissible RS conjunct2;
   21.28        in
   21.29          theory
   21.30          |> make_po (Tactic.rtac nonempty 1)
   21.31          |> make_cpo admissible
   21.32 -        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
   21.33 +        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
   21.34        end;
   21.35    
   21.36    in (goal, if pcpo then pcpodef_result else cpodef_result) end
    22.1 --- a/src/Provers/clasimp.ML	Fri Jan 20 04:53:59 2006 +0100
    22.2 +++ b/src/Provers/clasimp.ML	Sat Jan 21 23:02:14 2006 +0100
    22.3 @@ -56,12 +56,12 @@
    22.4    val fast_simp_tac: clasimpset -> int -> tactic
    22.5    val slow_simp_tac: clasimpset -> int -> tactic
    22.6    val best_simp_tac: clasimpset -> int -> tactic
    22.7 -  val attrib: (clasimpset * thm list -> clasimpset) -> Context.generic attribute
    22.8 +  val attrib: (clasimpset * thm list -> clasimpset) -> attribute
    22.9    val get_local_clasimpset: Proof.context -> clasimpset
   22.10    val local_clasimpset_of: Proof.context -> clasimpset
   22.11 -  val iff_add: Context.generic attribute
   22.12 -  val iff_add': Context.generic attribute
   22.13 -  val iff_del: Context.generic attribute
   22.14 +  val iff_add: attribute
   22.15 +  val iff_add': attribute
   22.16 +  val iff_del: attribute
   22.17    val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   22.18    val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   22.19    val setup: theory -> theory
   22.20 @@ -151,7 +151,7 @@
   22.21    end;
   22.22  
   22.23  fun modifier att (x, ths) =
   22.24 -  fst (Thm.applys_attributes [att] (x, rev ths));
   22.25 +  fst (foldl_map (Library.apply [att]) (x, rev ths));
   22.26  
   22.27  val addXIs = modifier (ContextRules.intro_query NONE);
   22.28  val addXEs = modifier (ContextRules.elim_query NONE);
   22.29 @@ -265,7 +265,7 @@
   22.30  
   22.31  (* attributes *)
   22.32  
   22.33 -fun attrib f = Attrib.declaration (fn th =>
   22.34 +fun attrib f = Thm.declaration_attribute (fn th =>
   22.35   fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
   22.36    | Context.Proof ctxt =>
   22.37        let
   22.38 @@ -295,10 +295,9 @@
   22.39  val iffN = "iff";
   22.40  
   22.41  val iff_modifiers =
   22.42 - [Args.$$$ iffN -- Scan.option Args.add -- Args.colon
   22.43 -    >> K ((I, Attrib.context iff_add): Method.modifier),
   22.44 -  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, Attrib.context iff_add'),
   22.45 -  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, Attrib.context iff_del)];
   22.46 + [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
   22.47 +  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
   22.48 +  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
   22.49  
   22.50  val clasimp_modifiers =
   22.51    Simplifier.simp_modifiers @ Splitter.split_modifiers @
   22.52 @@ -328,7 +327,7 @@
   22.53  
   22.54  val setup =
   22.55   (Attrib.add_attributes
   22.56 -   [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")] #>
   22.57 +   [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
   22.58    Method.add_methods
   22.59     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   22.60      ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
    23.1 --- a/src/Provers/classical.ML	Fri Jan 20 04:53:59 2006 +0100
    23.2 +++ b/src/Provers/classical.ML	Sat Jan 21 23:02:14 2006 +0100
    23.3 @@ -143,13 +143,13 @@
    23.4    val print_local_claset: Proof.context -> unit
    23.5    val get_local_claset: Proof.context -> claset
    23.6    val put_local_claset: claset -> Proof.context -> Proof.context
    23.7 -  val safe_dest: int option -> Context.generic attribute
    23.8 -  val safe_elim: int option -> Context.generic attribute
    23.9 -  val safe_intro: int option -> Context.generic attribute
   23.10 -  val haz_dest: int option -> Context.generic attribute
   23.11 -  val haz_elim: int option -> Context.generic attribute
   23.12 -  val haz_intro: int option -> Context.generic attribute
   23.13 -  val rule_del: Context.generic attribute
   23.14 +  val safe_dest: int option -> attribute
   23.15 +  val safe_elim: int option -> attribute
   23.16 +  val safe_intro: int option -> attribute
   23.17 +  val haz_dest: int option -> attribute
   23.18 +  val haz_elim: int option -> attribute
   23.19 +  val haz_intro: int option -> attribute
   23.20 +  val rule_del: attribute
   23.21    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   23.22    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   23.23    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   23.24 @@ -949,7 +949,7 @@
   23.25  
   23.26  (* attributes *)
   23.27  
   23.28 -fun attrib f = Attrib.declaration (fn th =>
   23.29 +fun attrib f = Thm.declaration_attribute (fn th =>
   23.30     fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   23.31      | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   23.32  
   23.33 @@ -989,14 +989,14 @@
   23.34  val ruleN = "rule";
   23.35  
   23.36  val setup_attrs = Attrib.add_attributes
   23.37 - [("swapped", Attrib.common swapped, "classical swap of introduction rule"),
   23.38 -  (destN, Attrib.common (ContextRules.add_args safe_dest haz_dest ContextRules.dest_query),
   23.39 + [("swapped", swapped, "classical swap of introduction rule"),
   23.40 +  (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   23.41      "declaration of Classical destruction rule"),
   23.42 -  (elimN, Attrib.common (ContextRules.add_args safe_elim haz_elim ContextRules.elim_query),
   23.43 +  (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   23.44      "declaration of Classical elimination rule"),
   23.45 -  (introN, Attrib.common (ContextRules.add_args safe_intro haz_intro ContextRules.intro_query),
   23.46 +  (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   23.47      "declaration of Classical introduction rule"),
   23.48 -  (ruleN, Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
   23.49 +  (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   23.50      "remove declaration of intro/elim/dest rule")];
   23.51  
   23.52  
   23.53 @@ -1044,13 +1044,13 @@
   23.54  (* automatic methods *)
   23.55  
   23.56  val cla_modifiers =
   23.57 - [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context (safe_dest NONE)): Method.modifier),
   23.58 -  Args.$$$ destN -- Args.colon >> K (I, Attrib.context (haz_dest NONE)),
   23.59 -  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context (safe_elim NONE)),
   23.60 -  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context (haz_elim NONE)),
   23.61 -  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context (safe_intro NONE)),
   23.62 -  Args.$$$ introN -- Args.colon >> K (I, Attrib.context (haz_intro NONE)),
   23.63 -  Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
   23.64 + [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
   23.65 +  Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
   23.66 +  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
   23.67 +  Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
   23.68 +  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
   23.69 +  Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   23.70 +  Args.del -- Args.colon >> K (I, rule_del)];
   23.71  
   23.72  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   23.73    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
    24.1 --- a/src/Provers/splitter.ML	Fri Jan 20 04:53:59 2006 +0100
    24.2 +++ b/src/Provers/splitter.ML	Sat Jan 21 23:02:14 2006 +0100
    24.3 @@ -32,8 +32,8 @@
    24.4    val delsplits       : simpset * thm list -> simpset
    24.5    val Addsplits       : thm list -> unit
    24.6    val Delsplits       : thm list -> unit
    24.7 -  val split_add: Context.generic attribute
    24.8 -  val split_del: Context.generic attribute
    24.9 +  val split_add: attribute
   24.10 +  val split_del: attribute
   24.11    val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
   24.12    val setup: theory -> theory
   24.13  end;
   24.14 @@ -443,9 +443,9 @@
   24.15  (* methods *)
   24.16  
   24.17  val split_modifiers =
   24.18 - [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
   24.19 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
   24.20 -  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
   24.21 + [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
   24.22 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
   24.23 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
   24.24  
   24.25  fun split_meth src =
   24.26    Method.syntax Attrib.local_thms src
   24.27 @@ -456,8 +456,7 @@
   24.28  
   24.29  val setup =
   24.30   (Attrib.add_attributes
   24.31 -  [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
   24.32 -    "declaration of case split rule")] #>
   24.33 +  [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
   24.34    Method.add_methods [(splitN, split_meth, "apply case split rule")]);
   24.35  
   24.36  end;
    25.1 --- a/src/Pure/Isar/args.ML	Fri Jan 20 04:53:59 2006 +0100
    25.2 +++ b/src/Pure/Isar/args.ML	Sat Jan 21 23:02:14 2006 +0100
    25.3 @@ -8,8 +8,8 @@
    25.4  
    25.5  signature ARGS =
    25.6  sig
    25.7 -  datatype value = Name of string | Typ of typ | Term of term | Fact of thm list |
    25.8 -    Attribute of Context.generic attribute
    25.9 +  datatype value =
   25.10 +    Name of string | Typ of typ | Term of term | Fact of thm list | Attribute of attribute
   25.11    type T
   25.12    val string_of: T -> string
   25.13    val mk_ident: string * Position.T -> T
   25.14 @@ -20,7 +20,7 @@
   25.15    val mk_typ: typ -> T
   25.16    val mk_term: term -> T
   25.17    val mk_fact: thm list -> T
   25.18 -  val mk_attribute: Context.generic attribute -> T
   25.19 +  val mk_attribute: attribute -> T
   25.20    val stopper: T * (T -> bool)
   25.21    val not_eof: T -> bool
   25.22    type src
   25.23 @@ -64,7 +64,7 @@
   25.24    val internal_typ: T list -> typ * T list
   25.25    val internal_term: T list -> term * T list
   25.26    val internal_fact: T list -> thm list * T list
   25.27 -  val internal_attribute: T list -> Context.generic attribute * T list
   25.28 +  val internal_attribute: T list -> attribute * T list
   25.29    val named_name: (string -> string) -> T list -> string * T list
   25.30    val named_typ: (string -> typ) -> T list -> typ * T list
   25.31    val named_term: (string -> term) -> T list -> term * T list
   25.32 @@ -118,7 +118,7 @@
   25.33    Typ of typ |
   25.34    Term of term |
   25.35    Fact of thm list |
   25.36 -  Attribute of Context.generic attribute;
   25.37 +  Attribute of attribute;
   25.38  
   25.39  datatype slot =
   25.40    Empty |
    26.1 --- a/src/Pure/Isar/calculation.ML	Fri Jan 20 04:53:59 2006 +0100
    26.2 +++ b/src/Pure/Isar/calculation.ML	Sat Jan 21 23:02:14 2006 +0100
    26.3 @@ -9,11 +9,11 @@
    26.4  sig
    26.5    val print_rules: Context.generic -> unit
    26.6    val get_calculation: Proof.state -> thm list option
    26.7 -  val trans_add: Context.generic attribute
    26.8 -  val trans_del: Context.generic attribute
    26.9 -  val sym_add: Context.generic attribute
   26.10 -  val sym_del: Context.generic attribute
   26.11 -  val symmetric: Context.generic attribute
   26.12 +  val trans_add: attribute
   26.13 +  val trans_del: attribute
   26.14 +  val sym_add: attribute
   26.15 +  val sym_del: attribute
   26.16 +  val symmetric: attribute
   26.17    val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   26.18    val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   26.19    val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   26.20 @@ -60,9 +60,8 @@
   26.21  val calculationN = "calculation";
   26.22  
   26.23  fun put_calculation calc =
   26.24 -  `Proof.level #-> (fn lev =>
   26.25 -    Proof.map_context (Context.the_proof o
   26.26 -        CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
   26.27 +  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
   26.28 +     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
   26.29    #> Proof.put_thms (calculationN, calc);
   26.30  
   26.31  
   26.32 @@ -71,20 +70,20 @@
   26.33  
   26.34  (* add/del rules *)
   26.35  
   26.36 -val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
   26.37 -val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
   26.38 +val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
   26.39 +val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
   26.40  
   26.41  val sym_add =
   26.42 -  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
   26.43 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
   26.44    #> ContextRules.elim_query NONE;
   26.45  val sym_del =
   26.46 -  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
   26.47 +  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
   26.48    #> ContextRules.rule_del;
   26.49  
   26.50  
   26.51  (* symmetric *)
   26.52  
   26.53 -val symmetric = Attrib.rule (fn x => fn th =>
   26.54 +val symmetric = Thm.rule_attribute (fn x => fn th =>
   26.55    (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
   26.56      ([th'], _) => th'
   26.57    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   26.58 @@ -98,12 +97,12 @@
   26.59  
   26.60  val _ = Context.add_setup
   26.61   (Attrib.add_attributes
   26.62 -   [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
   26.63 -    ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
   26.64 -    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
   26.65 +   [("trans", trans_att, "declaration of transitivity rule"),
   26.66 +    ("sym", sym_att, "declaration of symmetry rule"),
   26.67 +    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
   26.68    PureThy.add_thms
   26.69 -   [(("", transitive_thm), [Attrib.theory trans_add]),
   26.70 -    (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
   26.71 +   [(("", transitive_thm), [trans_add]),
   26.72 +    (("", symmetric_thm), [sym_add])] #> snd);
   26.73  
   26.74  
   26.75  
    27.1 --- a/src/Pure/Isar/constdefs.ML	Fri Jan 20 04:53:59 2006 +0100
    27.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Jan 21 23:02:14 2006 +0100
    27.3 @@ -13,7 +13,7 @@
    27.4      ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
    27.5      theory -> theory
    27.6    val add_constdefs_i: (string * typ option) list *
    27.7 -    ((bstring * typ option * mixfix) option * ((bstring * theory attribute list) * term)) list ->
    27.8 +    ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
    27.9      theory -> theory
   27.10  end;
   27.11  
   27.12 @@ -66,7 +66,7 @@
   27.13    in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
   27.14  
   27.15  val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
   27.16 -  ProofContext.read_term_legacy Attrib.global_attribute;
   27.17 +  ProofContext.read_term_legacy Attrib.attribute;
   27.18  val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
   27.19  
   27.20  end;
    28.1 --- a/src/Pure/Isar/context_rules.ML	Fri Jan 20 04:53:59 2006 +0100
    28.2 +++ b/src/Pure/Isar/context_rules.ML	Sat Jan 21 23:02:14 2006 +0100
    28.3 @@ -2,8 +2,8 @@
    28.4      ID:         $Id$
    28.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    28.6  
    28.7 -Declarations of intro/elim/dest rules in Pure; see
    28.8 -Provers/classical.ML for a more specialized version of the same idea.
    28.9 +Declarations of intro/elim/dest rules in Pure (see also
   28.10 +Provers/classical.ML for a more specialized version of the same idea).
   28.11  *)
   28.12  
   28.13  signature CONTEXT_RULES =
   28.14 @@ -20,18 +20,19 @@
   28.15    val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
   28.16    val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
   28.17    val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
   28.18 -  val intro_bang: int option -> Context.generic attribute
   28.19 -  val elim_bang: int option -> Context.generic attribute
   28.20 -  val dest_bang: int option -> Context.generic attribute
   28.21 -  val intro: int option -> Context.generic attribute
   28.22 -  val elim: int option -> Context.generic attribute
   28.23 -  val dest: int option -> Context.generic attribute
   28.24 -  val intro_query: int option -> Context.generic attribute
   28.25 -  val elim_query: int option -> Context.generic attribute
   28.26 -  val dest_query: int option -> Context.generic attribute
   28.27 -  val rule_del: Context.generic attribute
   28.28 -  val add_args: (int option -> 'a attribute) -> (int option -> 'a attribute) ->
   28.29 -    (int option -> 'a attribute) -> Attrib.src -> 'a attribute
   28.30 +  val intro_bang: int option -> attribute
   28.31 +  val elim_bang: int option -> attribute
   28.32 +  val dest_bang: int option -> attribute
   28.33 +  val intro: int option -> attribute
   28.34 +  val elim: int option -> attribute
   28.35 +  val dest: int option -> attribute
   28.36 +  val intro_query: int option -> attribute
   28.37 +  val elim_query: int option -> attribute
   28.38 +  val dest_query: int option -> attribute
   28.39 +  val rule_del: attribute
   28.40 +  val add_args:
   28.41 +    (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
   28.42 +    Attrib.src -> attribute
   28.43  end;
   28.44  
   28.45  structure ContextRules: CONTEXT_RULES =
   28.46 @@ -166,7 +167,7 @@
   28.47  (* wrappers *)
   28.48  
   28.49  fun gen_add_wrapper upd w =
   28.50 -  Context.map_theory (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   28.51 +  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
   28.52      make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
   28.53  
   28.54  val addSWrapper = gen_add_wrapper Library.apfst;
   28.55 @@ -203,7 +204,7 @@
   28.56  val dest_query  = rule_add elim_queryK Tactic.make_elim;
   28.57  
   28.58  val _ = Context.add_setup
   28.59 -  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
   28.60 +  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
   28.61  
   28.62  
   28.63  (* concrete syntax *)
   28.64 @@ -213,13 +214,10 @@
   28.65      >> (fn (f, n) => f n)) x;
   28.66  
   28.67  val rule_atts =
   28.68 - [("intro", Attrib.common (add_args intro_bang intro intro_query),
   28.69 -    "declaration of introduction rule"),
   28.70 -  ("elim", Attrib.common (add_args elim_bang elim elim_query),
   28.71 -    "declaration of elimination rule"),
   28.72 -  ("dest", Attrib.common (add_args dest_bang dest dest_query),
   28.73 -    "declaration of destruction rule"),
   28.74 -  ("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
   28.75 + [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
   28.76 +  ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
   28.77 +  ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
   28.78 +  ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
   28.79      "remove declaration of intro/elim/dest rule")];
   28.80  
   28.81  val _ = Context.add_setup (Attrib.add_attributes rule_atts);
    29.1 --- a/src/Pure/Isar/induct_attrib.ML	Fri Jan 20 04:53:59 2006 +0100
    29.2 +++ b/src/Pure/Isar/induct_attrib.ML	Sat Jan 21 23:02:14 2006 +0100
    29.3 @@ -25,12 +25,12 @@
    29.4    val find_inductS: Proof.context -> term -> thm list
    29.5    val find_coinductT: Proof.context -> typ -> thm list
    29.6    val find_coinductS: Proof.context -> term -> thm list
    29.7 -  val cases_type: string -> Context.generic attribute
    29.8 -  val cases_set: string -> Context.generic attribute
    29.9 -  val induct_type: string -> Context.generic attribute
   29.10 -  val induct_set: string -> Context.generic attribute
   29.11 -  val coinduct_type: string -> Context.generic attribute
   29.12 -  val coinduct_set: string -> Context.generic attribute
   29.13 +  val cases_type: string -> attribute
   29.14 +  val cases_set: string -> attribute
   29.15 +  val induct_type: string -> attribute
   29.16 +  val induct_set: string -> attribute
   29.17 +  val coinduct_type: string -> attribute
   29.18 +  val coinduct_set: string -> attribute
   29.19    val casesN: string
   29.20    val inductN: string
   29.21    val coinductN: string
   29.22 @@ -225,8 +225,8 @@
   29.23  
   29.24  val _ = Context.add_setup
   29.25   (Attrib.add_attributes
   29.26 -  [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
   29.27 -   (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
   29.28 -   (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]);
   29.29 +  [(casesN, cases_att, "declaration of cases rule for type or set"),
   29.30 +   (inductN, induct_att, "declaration of induction rule for type or set"),
   29.31 +   (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
   29.32  
   29.33  end;
    30.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jan 20 04:53:59 2006 +0100
    30.2 +++ b/src/Pure/Isar/isar_thy.ML	Sat Jan 21 23:02:14 2006 +0100
    30.3 @@ -8,16 +8,16 @@
    30.4  signature ISAR_THY =
    30.5  sig
    30.6    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    30.7 -  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    30.8 +  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory
    30.9    val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
   30.10 -  val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
   30.11 +  val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory
   30.12    val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
   30.13 -  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
   30.14 +  val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
   30.15    val theorems: string ->
   30.16      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
   30.17      -> theory -> (string * thm list) list * theory 
   30.18    val theorems_i: string ->
   30.19 -    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
   30.20 +    ((bstring * attribute list) * (thm list * attribute list) list) list
   30.21      -> theory -> (string * thm list) list * theory
   30.22    val smart_theorems: string -> xstring option ->
   30.23      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
   30.24 @@ -34,7 +34,7 @@
   30.25      bool -> Proof.state -> Proof.state
   30.26    val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
   30.27      theory -> Proof.state
   30.28 -  val theorem_i: string -> string * theory attribute list -> term * (term list * term list) ->
   30.29 +  val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
   30.30      theory -> Proof.state
   30.31    val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   30.32    val terminal_proof: Method.text * Method.text option ->
   30.33 @@ -58,7 +58,7 @@
   30.34  (* axioms and defs *)
   30.35  
   30.36  fun add_axms f args thy =
   30.37 -  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
   30.38 +  f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
   30.39  
   30.40  val add_axioms = add_axms (snd oo PureThy.add_axioms);
   30.41  val add_axioms_i = snd oo PureThy.add_axioms_i;
   30.42 @@ -73,7 +73,7 @@
   30.43      Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
   30.44  
   30.45  fun theorems kind args thy = thy
   30.46 -  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
   30.47 +  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.attribute thy) args)
   30.48    |> tap (present_theorems kind);
   30.49  
   30.50  fun theorems_i kind args =
    31.1 --- a/src/Pure/Isar/locale.ML	Fri Jan 20 04:53:59 2006 +0100
    31.2 +++ b/src/Pure/Isar/locale.ML	Sat Jan 21 23:02:14 2006 +0100
    31.3 @@ -72,7 +72,7 @@
    31.4  
    31.5    (* Storing results *)
    31.6    val smart_note_thmss: string -> string option ->
    31.7 -    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
    31.8 +    ((bstring * attribute list) * (thm list * attribute list) list) list ->
    31.9      theory -> (bstring * thm list) list * theory
   31.10    val note_thmss: string -> xstring ->
   31.11      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
   31.12 @@ -86,8 +86,8 @@
   31.13      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   31.14      theory -> Proof.state
   31.15    val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
   31.16 -    string * theory attribute list -> Element.context_i element list ->
   31.17 -    ((string * theory attribute list) * (term * (term list * term list)) list) list ->
   31.18 +    string * attribute list -> Element.context_i element list ->
   31.19 +    ((string * attribute list) * (term * (term list * term list)) list) list ->
   31.20      theory -> Proof.state
   31.21    val theorem_in_locale: string -> Method.text option ->
   31.22      (thm list list -> thm list list -> theory -> theory) ->
   31.23 @@ -838,7 +838,7 @@
   31.24        ((ctxt, mode), [])
   31.25    | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
   31.26        let
   31.27 -        val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
   31.28 +        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
   31.29          val ts = List.concat (map (map #1 o #2) asms');
   31.30          val (ps, qs) = splitAt (length ts, axs);
   31.31          val (_, ctxt') =
   31.32 @@ -849,7 +849,7 @@
   31.33        ((ctxt, Derived ths), [])
   31.34    | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
   31.35        let
   31.36 -        val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
   31.37 +        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   31.38          val (_, ctxt') =
   31.39          ctxt |> ProofContext.add_assms_i ProofContext.def_export
   31.40            (defs' |> map (fn ((name, atts), (t, ps)) =>
   31.41 @@ -860,7 +860,7 @@
   31.42        ((ctxt, Derived ths), [])
   31.43    | activate_elem is_ext ((ctxt, mode), Notes facts) =
   31.44        let
   31.45 -        val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
   31.46 +        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
   31.47          val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
   31.48        in ((ctxt', mode), if is_ext then res else []) end;
   31.49  
   31.50 @@ -1445,7 +1445,7 @@
   31.51              (Element.inst_term insts) (Element.inst_thm thy insts);
   31.52          val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
   31.53              ((NameSpace.qualified prfx n,
   31.54 -              map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)),
   31.55 +              map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
   31.56               [(map (Drule.standard o satisfy_protected prems o
   31.57              Element.inst_thm thy insts) ths, [])]));
   31.58        in global_note_accesses_i (Drule.kind kind) prfx args' thy |> snd end;
   31.59 @@ -1777,7 +1777,7 @@
   31.60  
   31.61  in
   31.62  
   31.63 -val theorem = gen_theorem Attrib.global_attribute intern_attrib read_context_statement;
   31.64 +val theorem = gen_theorem Attrib.attribute intern_attrib read_context_statement;
   31.65  val theorem_i = gen_theorem (K I) (K I) cert_context_statement;
   31.66  
   31.67  val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib
   31.68 @@ -1875,7 +1875,7 @@
   31.69        (fn thy => fn (name, ps) =>
   31.70          get_global_registration thy (name, map Logic.varify ps))
   31.71        (swap ooo global_note_accesses_i (Drule.kind ""))
   31.72 -      Attrib.global_attribute_i Drule.standard
   31.73 +      Attrib.attribute_i Drule.standard
   31.74        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
   31.75        (fn (n, ps) => fn (t, th) =>
   31.76           add_global_witness (n, map Logic.varify ps)
   31.77 @@ -1884,7 +1884,7 @@
   31.78  fun local_activate_facts_elemss x = gen_activate_facts_elemss
   31.79        get_local_registration
   31.80        local_note_accesses_i
   31.81 -      Attrib.context_attribute_i I
   31.82 +      (Attrib.attribute_i o ProofContext.theory_of) I
   31.83        put_local_registration
   31.84        add_local_witness x;
   31.85  
   31.86 @@ -2067,11 +2067,11 @@
   31.87              fun activate_elem (Notes facts) thy =
   31.88                  let
   31.89                    val facts' = facts
   31.90 -                      |> Attrib.map_facts (Attrib.global_attribute_i thy o
   31.91 +                      |> Attrib.map_facts (Attrib.attribute_i thy o
   31.92                           Args.map_values I (Element.instT_type (#1 insts))
   31.93                             (Element.inst_term insts)
   31.94                             (disch o Element.inst_thm thy insts o satisfy))
   31.95 -                      |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
   31.96 +                      |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
   31.97                        |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   31.98                        |> map (apfst (apfst (NameSpace.qualified prfx)))
   31.99                  in
    32.1 --- a/src/Pure/Isar/method.ML	Fri Jan 20 04:53:59 2006 +0100
    32.2 +++ b/src/Pure/Isar/method.ML	Sat Jan 21 23:02:14 2006 +0100
    32.3 @@ -581,7 +581,7 @@
    32.4  
    32.5  val add_method = add_methods o Library.single;
    32.6  
    32.7 -fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
    32.8 +fun Method name meth cmt = Context.>> (add_method (name, meth, cmt));
    32.9  
   32.10  
   32.11  (* method_setup *)
   32.12 @@ -615,7 +615,7 @@
   32.13  
   32.14  (* sections *)
   32.15  
   32.16 -type modifier = (ProofContext.context -> ProofContext.context) * ProofContext.context attribute;
   32.17 +type modifier = (ProofContext.context -> ProofContext.context) * attribute;
   32.18  
   32.19  local
   32.20  
   32.21 @@ -623,7 +623,7 @@
   32.22  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
   32.23  fun thmss ss = Scan.repeat (thms ss) >> List.concat;
   32.24  
   32.25 -fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
   32.26 +fun apply (f, att) (ctxt, ths) = foldl_map (Thm.proof_attributes [att]) (f ctxt, ths);
   32.27  
   32.28  fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
   32.29    Scan.succeed (apply m (ctxt, ths)))) >> #2;
   32.30 @@ -662,13 +662,13 @@
   32.31      >> (pair (I: ProofContext.context -> ProofContext.context) o att);
   32.32  
   32.33  val iprover_modifiers =
   32.34 - [modifier destN Args.bang_colon Args.bang (Attrib.context o ContextRules.dest_bang),
   32.35 -  modifier destN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.dest),
   32.36 -  modifier elimN Args.bang_colon Args.bang (Attrib.context o ContextRules.elim_bang),
   32.37 -  modifier elimN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.elim),
   32.38 -  modifier introN Args.bang_colon Args.bang (Attrib.context o ContextRules.intro_bang),
   32.39 -  modifier introN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.intro),
   32.40 -  Args.del -- Args.colon >> K (I, Attrib.context ContextRules.rule_del)];
   32.41 + [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
   32.42 +  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
   32.43 +  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
   32.44 +  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
   32.45 +  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
   32.46 +  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
   32.47 +  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
   32.48  
   32.49  in
   32.50  
    33.1 --- a/src/Pure/Isar/object_logic.ML	Fri Jan 20 04:53:59 2006 +0100
    33.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jan 21 23:02:14 2006 +0100
    33.3 @@ -14,8 +14,8 @@
    33.4    val drop_judgment: theory -> term -> term
    33.5    val fixed_judgment: theory -> string -> term
    33.6    val ensure_propT: theory -> term -> term
    33.7 -  val declare_atomize: theory attribute
    33.8 -  val declare_rulify: theory attribute
    33.9 +  val declare_atomize: attribute
   33.10 +  val declare_rulify: attribute
   33.11    val atomize_term: theory -> term -> term
   33.12    val atomize_cterm: theory -> cterm -> thm
   33.13    val atomize_thm: thm -> thm
   33.14 @@ -24,8 +24,8 @@
   33.15    val atomize_goal: int -> thm -> thm
   33.16    val rulify: thm -> thm
   33.17    val rulify_no_asm: thm -> thm
   33.18 -  val rule_format: 'a attribute
   33.19 -  val rule_format_no_asm: 'a attribute
   33.20 +  val rule_format: attribute
   33.21 +  val rule_format_no_asm: attribute
   33.22  end;
   33.23  
   33.24  structure ObjectLogic: OBJECT_LOGIC =
   33.25 @@ -123,11 +123,13 @@
   33.26  val get_atomize = #1 o #2 o ObjectLogicData.get;
   33.27  val get_rulify = #2 o #2 o ObjectLogicData.get;
   33.28  
   33.29 -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
   33.30 -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
   33.31 +val declare_atomize =
   33.32 +  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
   33.33 +    Library.apsnd o Library.apfst o Drule.add_rule);
   33.34  
   33.35 -fun declare_atomize (thy, th) = (add_atomize th thy, th);
   33.36 -fun declare_rulify (thy, th) = (add_rulify th thy, th);
   33.37 +val declare_rulify =
   33.38 +  Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
   33.39 +    Library.apsnd o Library.apsnd o Drule.add_rule);
   33.40  
   33.41  
   33.42  (* atomize *)
   33.43 @@ -164,8 +166,8 @@
   33.44  val rulify = gen_rulify true;
   33.45  val rulify_no_asm = gen_rulify false;
   33.46  
   33.47 -fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
   33.48 -fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   33.49 +fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
   33.50 +fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
   33.51  
   33.52  
   33.53  end;
    34.1 --- a/src/Pure/Isar/obtain.ML	Fri Jan 20 04:53:59 2006 +0100
    34.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 21 23:02:14 2006 +0100
    34.3 @@ -40,7 +40,7 @@
    34.4      ((string * Attrib.src list) * (string * (string list * string list)) list) list
    34.5      -> bool -> Proof.state -> Proof.state
    34.6    val obtain_i: (string * typ option) list ->
    34.7 -    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    34.8 +    ((string * attribute list) * (term * (term list * term list)) list) list
    34.9      -> bool -> Proof.state -> Proof.state
   34.10    val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
   34.11    val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
   34.12 @@ -137,7 +137,7 @@
   34.13      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   34.14      |> Proof.fix_i [(thesisN, NONE)]
   34.15      |> Proof.assume_i
   34.16 -      [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
   34.17 +      [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
   34.18      |> `Proof.the_facts
   34.19      ||> Proof.chain_facts chain_facts
   34.20      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
   34.21 @@ -146,7 +146,7 @@
   34.22  
   34.23  in
   34.24  
   34.25 -val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
   34.26 +val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
   34.27  val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   34.28  
   34.29  end;
    35.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 20 04:53:59 2006 +0100
    35.2 +++ b/src/Pure/Isar/proof.ML	Sat Jan 21 23:02:14 2006 +0100
    35.3 @@ -47,19 +47,19 @@
    35.4      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    35.5      state -> state
    35.6    val assm_i: ProofContext.export ->
    35.7 -    ((string * context attribute list) * (term * (term list * term list)) list) list
    35.8 +    ((string * attribute list) * (term * (term list * term list)) list) list
    35.9      -> state -> state
   35.10    val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   35.11      state -> state
   35.12 -  val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
   35.13 +  val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
   35.14      -> state -> state
   35.15    val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
   35.16      -> state -> state
   35.17 -  val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
   35.18 +  val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
   35.19      -> state -> state
   35.20    val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
   35.21      state -> state
   35.22 -  val def_i: ((string * context attribute list) * (string * (term * term list))) list ->
   35.23 +  val def_i: ((string * attribute list) * (string * (term * term list))) list ->
   35.24      state -> state
   35.25    val chain: state -> state
   35.26    val chain_facts: thm list -> state -> state
   35.27 @@ -67,18 +67,18 @@
   35.28    val simple_note_thms: string -> thm list -> state -> state
   35.29    val note_thmss: ((string * Attrib.src list) *
   35.30      (thmref * Attrib.src list) list) list -> state -> state
   35.31 -  val note_thmss_i: ((string * context attribute list) *
   35.32 -    (thm list * context attribute list) list) list -> state -> state
   35.33 +  val note_thmss_i: ((string * attribute list) *
   35.34 +    (thm list * attribute list) list) list -> state -> state
   35.35    val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
   35.36 -  val from_thmss_i: ((thm list * context attribute list) list) list -> state -> state
   35.37 +  val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   35.38    val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
   35.39 -  val with_thmss_i: ((thm list * context attribute list) list) list -> state -> state
   35.40 +  val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
   35.41    val using: ((thmref * Attrib.src list) list) list -> state -> state
   35.42 -  val using_i: ((thm list * context attribute list) list) list -> state -> state
   35.43 +  val using_i: ((thm list * attribute list) list) list -> state -> state
   35.44    val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
   35.45 -  val unfolding_i: ((thm list * context attribute list) list) list -> state -> state
   35.46 +  val unfolding_i: ((thm list * attribute list) list) list -> state -> state
   35.47    val invoke_case: string * string option list * Attrib.src list -> state -> state
   35.48 -  val invoke_case_i: string * string option list * context attribute list -> state -> state
   35.49 +  val invoke_case_i: string * string option list * attribute list -> state -> state
   35.50    val begin_block: state -> state
   35.51    val next_block: state -> state
   35.52    val end_block: state -> state Seq.seq
   35.53 @@ -89,13 +89,13 @@
   35.54    val apply_end: Method.text -> state -> state Seq.seq
   35.55    val goal_names: string option -> string -> string list -> string
   35.56    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
   35.57 -    (theory -> 'a -> context attribute) ->
   35.58 +    (theory -> 'a -> attribute) ->
   35.59      (context * 'b list -> context * (term list list * (context -> context))) ->
   35.60      string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
   35.61      ((string * 'a list) * 'b) list -> state -> state
   35.62    val local_qed: Method.text option * bool -> state -> state Seq.seq
   35.63    val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
   35.64 -    (theory -> 'a -> theory attribute) ->
   35.65 +    (theory -> 'a -> attribute) ->
   35.66      (context * 'b list -> context * (term list list * (context -> context))) ->
   35.67      string -> Method.text option -> (thm list list -> theory -> theory) ->
   35.68      string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
   35.69 @@ -114,21 +114,21 @@
   35.70      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   35.71      bool -> state -> state
   35.72    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   35.73 -    ((string * context attribute list) * (term * (term list * term list)) list) list ->
   35.74 +    ((string * attribute list) * (term * (term list * term list)) list) list ->
   35.75      bool -> state -> state
   35.76    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   35.77      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   35.78      bool -> state -> state
   35.79    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   35.80 -    ((string * context attribute list) * (term * (term list * term list)) list) list ->
   35.81 +    ((string * attribute list) * (term * (term list * term list)) list) list ->
   35.82      bool -> state -> state
   35.83    val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
   35.84      string option -> string * Attrib.src list ->
   35.85      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   35.86      context -> state
   35.87    val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
   35.88 -    string option -> string * theory attribute list ->
   35.89 -    ((string * theory attribute list) * (term * (term list * term list)) list) list ->
   35.90 +    string option -> string * attribute list ->
   35.91 +    ((string * attribute list) * (term * (term list * term list)) list) list ->
   35.92      context -> state
   35.93  end;
   35.94  
   35.95 @@ -534,7 +534,7 @@
   35.96  
   35.97  in
   35.98  
   35.99 -val assm      = gen_assume ProofContext.add_assms Attrib.local_attribute;
  35.100 +val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
  35.101  val assm_i    = gen_assume ProofContext.add_assms_i (K I);
  35.102  val assume    = assm ProofContext.assume_export;
  35.103  val assume_i  = assm_i ProofContext.assume_export;
  35.104 @@ -566,7 +566,7 @@
  35.105  
  35.106  in
  35.107  
  35.108 -val def = gen_def fix Attrib.local_attribute ProofContext.match_bind;
  35.109 +val def = gen_def fix Attrib.attribute ProofContext.match_bind;
  35.110  val def_i = gen_def fix_i (K I) ProofContext.match_bind_i;
  35.111  
  35.112  end;
  35.113 @@ -603,15 +603,15 @@
  35.114  
  35.115  in
  35.116  
  35.117 -val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.local_attribute;
  35.118 +val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.attribute;
  35.119  val note_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) I #2 (K I);
  35.120  
  35.121  val from_thmss =
  35.122 -  gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.local_attribute o no_binding;
  35.123 +  gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.attribute o no_binding;
  35.124  val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain #2 (K I) o no_binding;
  35.125  
  35.126  val with_thmss =
  35.127 -  gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.local_attribute o no_binding;
  35.128 +  gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.attribute o no_binding;
  35.129  val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain #2 (K I) o no_binding;
  35.130  
  35.131  val local_results = gen_thmss ProofContext.note_thmss_i (K []) I I (K I);
  35.132 @@ -642,9 +642,9 @@
  35.133  
  35.134  in
  35.135  
  35.136 -val using = gen_using append_using (K I) ProofContext.note_thmss Attrib.local_attribute;
  35.137 +val using = gen_using append_using (K I) ProofContext.note_thmss Attrib.attribute;
  35.138  val using_i = gen_using append_using (K I) ProofContext.note_thmss_i (K I);
  35.139 -val unfolding = gen_using unfold_using unfold_goal ProofContext.note_thmss Attrib.local_attribute;
  35.140 +val unfolding = gen_using unfold_using unfold_goal ProofContext.note_thmss Attrib.attribute;
  35.141  val unfolding_i = gen_using unfold_using unfold_goal ProofContext.note_thmss_i (K I);
  35.142  
  35.143  end;
  35.144 @@ -671,7 +671,7 @@
  35.145  
  35.146  in
  35.147  
  35.148 -val invoke_case = gen_invoke_case Attrib.local_attribute;
  35.149 +val invoke_case = gen_invoke_case Attrib.attribute;
  35.150  val invoke_case_i = gen_invoke_case (K I);
  35.151  
  35.152  end;
  35.153 @@ -957,11 +957,11 @@
  35.154  
  35.155  in
  35.156  
  35.157 -val have = gen_have Attrib.local_attribute ProofContext.bind_propp;
  35.158 +val have = gen_have Attrib.attribute ProofContext.bind_propp;
  35.159  val have_i = gen_have (K I) ProofContext.bind_propp_i;
  35.160 -val show = gen_show Attrib.local_attribute ProofContext.bind_propp;
  35.161 +val show = gen_show Attrib.attribute ProofContext.bind_propp;
  35.162  val show_i = gen_show (K I) ProofContext.bind_propp_i;
  35.163 -val theorem = gen_theorem Attrib.global_attribute ProofContext.bind_propp_schematic;
  35.164 +val theorem = gen_theorem Attrib.attribute ProofContext.bind_propp_schematic;
  35.165  val theorem_i = gen_theorem (K I) ProofContext.bind_propp_schematic_i;
  35.166  
  35.167  end;
    36.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jan 20 04:53:59 2006 +0100
    36.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jan 21 23:02:14 2006 +0100
    36.3 @@ -109,10 +109,10 @@
    36.4    val hide_thms: bool -> string list -> context -> context
    36.5    val put_thms: string * thm list option -> context -> context
    36.6    val note_thmss:
    36.7 -    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
    36.8 +    ((bstring * attribute list) * (thmref * attribute list) list) list ->
    36.9        context -> (bstring * thm list) list * context
   36.10    val note_thmss_i:
   36.11 -    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
   36.12 +    ((bstring * attribute list) * (thm list * attribute list) list) list ->
   36.13        context -> (bstring * thm list) list * context
   36.14    val read_vars: (string * string option * mixfix) list -> context ->
   36.15      (string * typ option * mixfix) list * context
   36.16 @@ -129,10 +129,10 @@
   36.17    val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
   36.18    val bind_fixes: string list -> context -> (term -> term) * context
   36.19    val add_assms: export ->
   36.20 -    ((string * context attribute list) * (string * (string list * string list)) list) list ->
   36.21 +    ((string * attribute list) * (string * (string list * string list)) list) list ->
   36.22      context -> (bstring * thm list) list * context
   36.23    val add_assms_i: export ->
   36.24 -    ((string * context attribute list) * (term * (term list * term list)) list) list ->
   36.25 +    ((string * attribute list) * (term * (term list * term list)) list) list ->
   36.26      context -> (bstring * thm list) list * context
   36.27    val assume_export: export
   36.28    val presume_export: export
   36.29 @@ -1042,7 +1042,7 @@
   36.30  fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
   36.31    let
   36.32      fun app (th, attrs) (ct, ths) =
   36.33 -      let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th)
   36.34 +      let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th)
   36.35        in (ct', th' :: ths) end;
   36.36      val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
   36.37      val thms = List.concat (rev rev_thms);
    37.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Jan 20 04:53:59 2006 +0100
    37.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 21 23:02:14 2006 +0100
    37.3 @@ -33,15 +33,15 @@
    37.4    val consume: thm list -> thm list -> ('a * int) * thm ->
    37.5      (('a * (int * thm list)) * thm) Seq.seq
    37.6    val add_consumes: int -> thm -> thm
    37.7 -  val consumes: int -> 'a attribute
    37.8 -  val consumes_default: int -> 'a attribute
    37.9 +  val consumes: int -> attribute
   37.10 +  val consumes_default: int -> attribute
   37.11    val name: string list -> thm -> thm
   37.12 -  val case_names: string list -> 'a attribute
   37.13 -  val case_conclusion: string * string list -> 'a attribute
   37.14 +  val case_names: string list -> attribute
   37.15 +  val case_conclusion: string * string list -> attribute
   37.16    val save: thm -> thm -> thm
   37.17    val get: thm -> (string * string list) list * int
   37.18    val rename_params: string list list -> thm -> thm
   37.19 -  val params: string list list -> 'a attribute
   37.20 +  val params: string list list -> attribute
   37.21    val mutual_rule: thm list -> (int list * thm) option
   37.22    val strict_mutual_rule: thm list -> int list * thm
   37.23  end;
   37.24 @@ -232,7 +232,7 @@
   37.25  
   37.26  val save_consumes = put_consumes o lookup_consumes;
   37.27  
   37.28 -fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
   37.29 +fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
   37.30  fun consumes_default n x =
   37.31    if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
   37.32  
   37.33 @@ -251,7 +251,7 @@
   37.34  
   37.35  val save_case_names = add_case_names o lookup_case_names;
   37.36  val name = add_case_names o SOME;
   37.37 -fun case_names ss = Drule.rule_attribute (K (name ss));
   37.38 +fun case_names ss = Thm.rule_attribute (K (name ss));
   37.39  
   37.40  
   37.41  
   37.42 @@ -277,7 +277,7 @@
   37.43      | _ => NONE)
   37.44    in fold add_case_concl concls end;
   37.45  
   37.46 -fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
   37.47 +fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
   37.48  
   37.49  
   37.50  
   37.51 @@ -304,7 +304,7 @@
   37.52    |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   37.53    |> save th;
   37.54  
   37.55 -fun params xss = Drule.rule_attribute (K (rename_params xss));
   37.56 +fun params xss = Thm.rule_attribute (K (rename_params xss));
   37.57  
   37.58  
   37.59  
    38.1 --- a/src/Pure/Isar/specification.ML	Fri Jan 20 04:53:59 2006 +0100
    38.2 +++ b/src/Pure/Isar/specification.ML	Sat Jan 21 23:02:14 2006 +0100
    38.3 @@ -13,18 +13,18 @@
    38.4      (string * string option * mixfix) list *
    38.5        ((string * Attrib.src list) * string list) list -> Proof.context ->
    38.6      ((string * typ * mixfix) list *
    38.7 -      ((string * Context.generic attribute list) * term list) list) * Proof.context
    38.8 +      ((string * attribute list) * term list) list) * Proof.context
    38.9    val cert_specification:
   38.10      (string * typ option * mixfix) list *
   38.11 -      ((string * Context.generic attribute list) * term list) list -> Proof.context ->
   38.12 +      ((string * attribute list) * term list) list -> Proof.context ->
   38.13      ((string * typ * mixfix) list *
   38.14 -      ((string * Context.generic attribute list) * term list) list) * Proof.context
   38.15 +      ((string * attribute list) * term list) list) * Proof.context
   38.16    val axiomatize:
   38.17      (string * string option * mixfix) list *
   38.18        ((bstring * Attrib.src list) * string list) list -> theory -> thm list list * theory
   38.19    val axiomatize_i:
   38.20      (string * typ option * mixfix) list *
   38.21 -      ((bstring * Context.generic attribute list) * term list) list -> theory ->
   38.22 +      ((bstring * attribute list) * term list) list -> theory ->
   38.23      thm list list * theory
   38.24  end;
   38.25  
   38.26 @@ -61,7 +61,7 @@
   38.27    in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
   38.28  
   38.29  fun read_specification x =
   38.30 -  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.generic_attribute x;
   38.31 +  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.attribute x;
   38.32  fun cert_specification x =
   38.33    prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
   38.34  
   38.35 @@ -73,7 +73,7 @@
   38.36      val ((consts, specs), ctxt) = prep args (ProofContext.init thy);
   38.37      val subst = consts |> map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T)));
   38.38      val axioms = specs |> map (fn ((name, att), ts) =>
   38.39 -      ((name, map (Term.subst_atomic subst) ts), map Attrib.theory att));
   38.40 +      ((name, map (Term.subst_atomic subst) ts), att));
   38.41      val (thms, thy') =
   38.42        thy
   38.43        |> Theory.add_consts_i consts
    39.1 --- a/src/Pure/Proof/extraction.ML	Fri Jan 20 04:53:59 2006 +0100
    39.2 +++ b/src/Pure/Proof/extraction.ML	Sat Jan 21 23:02:14 2006 +0100
    39.3 @@ -355,7 +355,7 @@
    39.4  
    39.5  (** expanding theorems / definitions **)
    39.6  
    39.7 -fun add_expand_thm (thy, thm) =
    39.8 +fun add_expand_thm thm thy =
    39.9    let
   39.10      val {realizes_eqns, typeof_eqns, types, realizers,
   39.11        defs, expand, prep} = ExtractionData.get thy;
   39.12 @@ -379,10 +379,13 @@
   39.13        else
   39.14          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
   39.15           realizers = realizers, defs = defs,
   39.16 -         expand = (name, prop_of thm) ins expand, prep = prep}) thy, thm)
   39.17 +         expand = (name, prop_of thm) ins expand, prep = prep}) thy)
   39.18    end;
   39.19  
   39.20 -fun add_expand_thms thms thy = Library.foldl (fst o add_expand_thm) (thy, thms);
   39.21 +val add_expand_thms = fold add_expand_thm;
   39.22 +
   39.23 +val extraction_expand =
   39.24 +  Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm));
   39.25  
   39.26  
   39.27  (** types with computational content **)
   39.28 @@ -445,8 +448,7 @@
   39.29      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
   39.30  
   39.31     Attrib.add_attributes
   39.32 -     [("extraction_expand",
   39.33 -       (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
   39.34 +     [("extraction_expand", extraction_expand,
   39.35         "specify theorems / definitions to be expanded during extraction")]);
   39.36  
   39.37  
    40.1 --- a/src/Pure/Tools/class_package.ML	Fri Jan 20 04:53:59 2006 +0100
    40.2 +++ b/src/Pure/Tools/class_package.ML	Sat Jan 21 23:02:14 2006 +0100
    40.3 @@ -15,7 +15,7 @@
    40.4      -> ((bstring * string) * Attrib.src list) list
    40.5      -> theory -> Proof.state
    40.6    val add_instance_arity_i: (string * sort list) * sort
    40.7 -    -> ((bstring * term) * theory attribute list) list
    40.8 +    -> ((bstring * term) * attribute list) list
    40.9      -> theory -> Proof.state
   40.10    val add_classentry: class -> xstring list -> xstring list -> theory -> theory
   40.11  
    41.1 --- a/src/Pure/axclass.ML	Fri Jan 20 04:53:59 2006 +0100
    41.2 +++ b/src/Pure/axclass.ML	Sat Jan 21 23:02:14 2006 +0100
    41.3 @@ -12,7 +12,7 @@
    41.4    val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
    41.5    val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
    41.6      theory -> {intro: thm, axioms: thm list} * theory
    41.7 -  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
    41.8 +  val add_axclass_i: bstring * class list -> ((bstring * term) * attribute list) list ->
    41.9      theory -> {intro: thm, axioms: thm list} * theory
   41.10    val add_classrel_thms: thm list -> theory -> theory
   41.11    val add_arity_thms: thm list -> theory -> theory
   41.12 @@ -216,7 +216,7 @@
   41.13  
   41.14  in
   41.15  
   41.16 -val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
   41.17 +val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.attribute;
   41.18  val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
   41.19  
   41.20  end;
    42.1 --- a/src/Pure/codegen.ML	Fri Jan 20 04:53:59 2006 +0100
    42.2 +++ b/src/Pure/codegen.ML	Sat Jan 21 23:02:14 2006 +0100
    42.3 @@ -26,7 +26,7 @@
    42.4  
    42.5    val add_codegen: string -> term codegen -> theory -> theory
    42.6    val add_tycodegen: string -> typ codegen -> theory -> theory
    42.7 -  val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
    42.8 +  val add_attribute: string -> (Args.T list -> attribute * Args.T list) -> theory -> theory
    42.9    val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
   42.10    val preprocess: theory -> thm list -> thm list
   42.11    val preprocess_term: theory -> term -> term
   42.12 @@ -207,7 +207,7 @@
   42.13       tycodegens : (string * typ codegen) list,
   42.14       consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
   42.15       types : (string * (typ mixfix list * (string * string) list)) list,
   42.16 -     attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
   42.17 +     attrs: (string * (Args.T list -> attribute * Args.T list)) list,
   42.18       preprocs: (stamp * (theory -> thm list -> thm list)) list,
   42.19       modules: codegr Symtab.table,
   42.20       test_params: test_params};
   42.21 @@ -312,13 +312,11 @@
   42.22  fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
   42.23  
   42.24  val code_attr =
   42.25 -  Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
   42.26 -    (#attrs (CodegenData.get thy)))));
   42.27 +  Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
   42.28 +    (#attrs (CodegenData.get (Context.theory_of context))))));
   42.29  
   42.30  val _ = Context.add_setup
   42.31 - (Attrib.add_attributes
   42.32 -  [("code", (code_attr, K Attrib.undef_local_attribute),
   42.33 -     "declare theorems for code generation")]);
   42.34 +  (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
   42.35  
   42.36  
   42.37  (**** preprocessors ****)
   42.38 @@ -348,10 +346,9 @@
   42.39      | _ => err ()
   42.40    end;
   42.41  
   42.42 -fun unfold_attr (thy, eqn) =
   42.43 +val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory
   42.44    let
   42.45 -    val names = term_consts
   42.46 -      (fst (Logic.dest_equals (prop_of eqn)));
   42.47 +    val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
   42.48      fun prep thy = map (fn th =>
   42.49        let val prop = prop_of th
   42.50        in
   42.51 @@ -359,7 +356,7 @@
   42.52          then rewrite_rule [eqn] (Thm.transfer thy th)
   42.53          else th
   42.54        end)
   42.55 -  in (add_preprocessor prep thy, eqn) end;
   42.56 +  in add_preprocessor prep end);
   42.57  
   42.58  val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
   42.59  
    43.1 --- a/src/Pure/pure_thy.ML	Fri Jan 20 04:53:59 2006 +0100
    43.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 21 23:02:14 2006 +0100
    43.3 @@ -47,35 +47,30 @@
    43.4    val thms_of: theory -> (string * thm) list
    43.5    val all_thms_of: theory -> (string * thm) list
    43.6    val hide_thms: bool -> string list -> theory -> theory
    43.7 -  val store_thm: (bstring * thm) * theory attribute list -> theory -> thm * theory
    43.8 +  val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
    43.9    val smart_store_thms: (bstring * thm list) -> thm list
   43.10    val smart_store_thms_open: (bstring * thm list) -> thm list
   43.11    val forall_elim_var: int -> thm -> thm
   43.12    val forall_elim_vars: int -> thm -> thm
   43.13 -  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> thm list * theory
   43.14 -  val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
   43.15 -    -> thm list list * theory 
   43.16 -  val note_thmss: theory attribute -> ((bstring * theory attribute list) *
   43.17 -    (thmref * theory attribute list) list) list ->
   43.18 -    theory -> (bstring * thm list) list * theory
   43.19 -  val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
   43.20 -    (thm list * theory attribute list) list) list ->
   43.21 -    theory -> (bstring * thm list) list * theory
   43.22 -  val add_axioms: ((bstring * string) * theory attribute list) list ->
   43.23 +  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   43.24 +  val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory 
   43.25 +  val note_thmss: attribute -> ((bstring * attribute list) *
   43.26 +    (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   43.27 +  val note_thmss_i: attribute -> ((bstring * attribute list) *
   43.28 +    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   43.29 +  val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   43.30 +  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   43.31 +  val add_axiomss: ((bstring * string list) * attribute list) list ->
   43.32 +    theory -> thm list list * theory
   43.33 +  val add_axiomss_i: ((bstring * term list) * attribute list) list ->
   43.34 +    theory -> thm list list * theory
   43.35 +  val add_defs: bool -> ((bstring * string) * attribute list) list ->
   43.36      theory -> thm list * theory
   43.37 -  val add_axioms_i: ((bstring * term) * theory attribute list) list ->
   43.38 +  val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
   43.39      theory -> thm list * theory
   43.40 -  val add_axiomss: ((bstring * string list) * theory attribute list) list ->
   43.41 -    theory -> thm list list * theory
   43.42 -  val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
   43.43 +  val add_defss: bool -> ((bstring * string list) * attribute list) list ->
   43.44      theory -> thm list list * theory
   43.45 -  val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
   43.46 -    theory -> thm list * theory
   43.47 -  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
   43.48 -    theory -> thm list * theory
   43.49 -  val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
   43.50 -    theory -> thm list list * theory
   43.51 -  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
   43.52 +  val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
   43.53      theory -> thm list list * theory
   43.54    val generic_setup: string option -> theory -> theory
   43.55    val add_oracle: bstring * string * string -> theory -> theory
   43.56 @@ -340,8 +335,7 @@
   43.57  (* add_thms(s) *)
   43.58  
   43.59  fun add_thms_atts pre_name ((bname, thms), atts) =
   43.60 -  enter_thms pre_name (name_thms false)
   43.61 -    (Thm.applys_attributes atts) (bname, thms);
   43.62 +  enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms);
   43.63  
   43.64  fun gen_add_thmss pre_name =
   43.65    fold_map (add_thms_atts pre_name);
   43.66 @@ -359,7 +353,7 @@
   43.67  
   43.68  fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
   43.69    let
   43.70 -    fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
   43.71 +    fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
   43.72      val (thms, thy') = thy |> enter_thms
   43.73        name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
   43.74        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
    44.1 --- a/src/Pure/simplifier.ML	Fri Jan 20 04:53:59 2006 +0100
    44.2 +++ b/src/Pure/simplifier.ML	Sat Jan 21 23:02:14 2006 +0100
    44.3 @@ -64,11 +64,11 @@
    44.4    val print_local_simpset: Proof.context -> unit
    44.5    val get_local_simpset: Proof.context -> simpset
    44.6    val put_local_simpset: simpset -> Proof.context -> Proof.context
    44.7 -  val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
    44.8 -  val simp_add: Context.generic attribute
    44.9 -  val simp_del: Context.generic attribute
   44.10 -  val cong_add: Context.generic attribute
   44.11 -  val cong_del: Context.generic attribute
   44.12 +  val attrib: (simpset * thm list -> simpset) -> attribute
   44.13 +  val simp_add: attribute
   44.14 +  val simp_del: attribute
   44.15 +  val cong_add: attribute
   44.16 +  val cong_del: attribute
   44.17    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   44.18    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
   44.19    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   44.20 @@ -138,7 +138,7 @@
   44.21  
   44.22  (* attributes *)
   44.23  
   44.24 -fun attrib f = Attrib.declaration (fn th =>
   44.25 +fun attrib f = Thm.declaration_attribute (fn th =>
   44.26     fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
   44.27      | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
   44.28  
   44.29 @@ -251,7 +251,7 @@
   44.30  in
   44.31  
   44.32  val simplified =
   44.33 -  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
   44.34 +  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
   44.35      f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
   44.36  
   44.37  end;
   44.38 @@ -261,11 +261,9 @@
   44.39  
   44.40  val _ = Context.add_setup
   44.41   (Attrib.add_attributes
   44.42 -   [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   44.43 -      "declaration of Simplifier rule"),
   44.44 -    (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   44.45 -      "declaration of Simplifier congruence rule"),
   44.46 -    ("simplified", Attrib.common simplified, "simplified rule")]);
   44.47 +   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"),
   44.48 +    (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
   44.49 +    ("simplified", simplified, "simplified rule")]);
   44.50  
   44.51  
   44.52  
   44.53 @@ -286,23 +284,23 @@
   44.54    >> (curry (Library.foldl op o) I o rev)) x;
   44.55  
   44.56  val cong_modifiers =
   44.57 - [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
   44.58 -  Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
   44.59 -  Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
   44.60 + [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
   44.61 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
   44.62 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
   44.63  
   44.64  val simp_modifiers =
   44.65 - [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
   44.66 -  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
   44.67 -  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   44.68 + [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
   44.69 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   44.70 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
   44.71    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   44.72 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
   44.73 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
   44.74     @ cong_modifiers;
   44.75  
   44.76  val simp_modifiers' =
   44.77 - [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
   44.78 -  Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   44.79 + [Args.add -- Args.colon >> K (I, simp_add),
   44.80 +  Args.del -- Args.colon >> K (I, simp_del),
   44.81    Args.$$$ onlyN -- Args.colon
   44.82 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
   44.83 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
   44.84     @ cong_modifiers;
   44.85  
   44.86  fun simp_args more_mods =
    45.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Jan 20 04:53:59 2006 +0100
    45.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 21 23:02:14 2006 +0100
    45.3 @@ -367,8 +367,8 @@
    45.4    (*Updating theory components: simprules and datatype info*)
    45.5    (thy1 |> Theory.add_path big_rec_base_name
    45.6          |> PureThy.add_thmss
    45.7 -         [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
    45.8 -          (("", intrs), [Attrib.theory (Classical.safe_intro NONE)]),
    45.9 +         [(("simps", simps), [Simplifier.simp_add]),
   45.10 +          (("", intrs), [Classical.safe_intro NONE]),
   45.11            (("con_defs", con_defs), []),
   45.12            (("case_eqns", case_eqns), []),
   45.13            (("recursor_eqns", recursor_eqns), []),
    46.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jan 20 04:53:59 2006 +0100
    46.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Jan 21 23:02:14 2006 +0100
    46.3 @@ -53,7 +53,7 @@
    46.4      val read_prop = ProofContext.read_prop (ProofContext.init thy);
    46.5      val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    46.6      val facts = args |> map (fn ((name, srcs), props) =>
    46.7 -      ((name, map (Attrib.global_attribute thy) srcs),
    46.8 +      ((name, map (Attrib.attribute thy) srcs),
    46.9          map (Thm.no_attributes o single o mk_cases) props));
   46.10    in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
   46.11  
    47.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Jan 20 04:53:59 2006 +0100
    47.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jan 21 23:02:14 2006 +0100
    47.3 @@ -165,7 +165,7 @@
    47.4    in
    47.5      thy
    47.6      |> Theory.add_path (Sign.base_name big_rec_name)
    47.7 -    |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
    47.8 +    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
    47.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   47.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   47.11      |> Theory.parent_path
    48.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jan 20 04:53:59 2006 +0100
    48.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Jan 21 23:02:14 2006 +0100
    48.3 @@ -29,7 +29,7 @@
    48.4    (*Insert definitions for the recursive sets, which
    48.5       must *already* be declared as constants in parent theory!*)
    48.6    val add_inductive_i: bool -> term list * term ->
    48.7 -    ((bstring * term) * theory attribute list) list ->
    48.8 +    ((bstring * term) * attribute list) list ->
    48.9      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   48.10    val add_inductive: string list * string ->
   48.11      ((bstring * string) * Attrib.src list) list ->
   48.12 @@ -515,7 +515,7 @@
   48.13       val ([induct', mutual_induct'], thy') =
   48.14         thy
   48.15         |> PureThy.add_thms [((co_prefix ^ "induct", induct),
   48.16 -             [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]),
   48.17 +             [case_names, InductAttrib.induct_set big_rec_name]),
   48.18             (("mutual_induct", mutual_induct), [case_names])];
   48.19      in ((thy', induct'), mutual_induct')
   48.20      end;  (*of induction_rules*)
   48.21 @@ -537,7 +537,7 @@
   48.22      |> PureThy.add_thms
   48.23        [(("bnd_mono", bnd_mono), []),
   48.24         (("dom_subset", dom_subset), []),
   48.25 -       (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])]
   48.26 +       (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])]
   48.27      ||>> (PureThy.add_thmss o map Thm.no_attributes)
   48.28          [("defs", defs),
   48.29           ("intros", intrs)];
   48.30 @@ -561,7 +561,7 @@
   48.31  fun add_inductive (srec_tms, sdom_sum) intr_srcs
   48.32      (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   48.33    let
   48.34 -    val intr_atts = map (map (Attrib.global_attribute thy) o snd) intr_srcs;
   48.35 +    val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
   48.36      val sintrs = map fst intr_srcs ~~ intr_atts;
   48.37      val read = Sign.simple_read_term thy;
   48.38      val rec_tms = map (read Ind_Syntax.iT) srec_tms;
    49.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Jan 20 04:53:59 2006 +0100
    49.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Jan 21 23:02:14 2006 +0100
    49.3 @@ -11,7 +11,7 @@
    49.4  sig
    49.5    val quiet_mode: bool ref
    49.6    val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
    49.7 -  val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    49.8 +  val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
    49.9  end;
   49.10  
   49.11  structure PrimrecPackage : PRIMREC_PACKAGE =
   49.12 @@ -191,13 +191,13 @@
   49.13        |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   49.14      val (_, thy3) =
   49.15        thy2
   49.16 -      |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])]
   49.17 +      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
   49.18        ||> Theory.parent_path;
   49.19    in (thy3, eqn_thms') end;
   49.20  
   49.21  fun add_primrec args thy =
   49.22    add_primrec_i (map (fn ((name, s), srcs) =>
   49.23 -    ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs))
   49.24 +    ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.attribute thy) srcs))
   49.25      args) thy;
   49.26  
   49.27