# HG changeset patch
# User wenzelm
# Date 1137273934 -3600
# Node ID abf0f018b5ece7f68b890bc8b091112d5bce9f7d
# Parent  af605e1864803e031b9eb4bb4b65543e035fa21d
generic attributes;

diff -r af605e186480 -r abf0f018b5ec src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -350,10 +350,10 @@
                   weak_case_congs cong_att =
   (snd o PureThy.add_thmss [(("simps", simps), []),
     (("", List.concat case_thms @ size_thms @ 
-          List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
+          List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
     (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
-    (("", List.concat inject),               [iff_add_global]),
-    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim_global]),
+    (("", List.concat inject),               [Attrib.theory iff_add]),
+    (("", map name_notE (List.concat distinct)),  [Attrib.theory Classical.safe_elim]),
     (("", weak_case_congs),                  [cong_att])]);
 
 
@@ -747,7 +747,7 @@
       |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
       |> Theory.add_path (space_implode "_" new_type_names)
       |> add_rules simps case_thms size_thms rec_thms inject distinct
-           weak_case_congs Simplifier.cong_add_global
+           weak_case_congs (Attrib.theory Simplifier.cong_add)
       |> put_datatypes (fold Symtab.update dt_infos dt_info)
       |> add_cases_induct dt_infos induct
       |> Theory.parent_path
@@ -806,7 +806,7 @@
       |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
       |> Theory.add_path (space_implode "_" new_type_names)
       |> add_rules simps case_thms size_thms rec_thms inject distinct
-            weak_case_congs (Simplifier.change_global_ss (op addcongs))
+            weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
       |> put_datatypes (fold Symtab.update dt_infos dt_info)
       |> add_cases_induct dt_infos induct
       |> Theory.parent_path
@@ -913,7 +913,7 @@
     val thy11 = thy10 |>
       Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
       add_rules simps case_thms size_thms rec_thms inject distinct
-                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
+                weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |> 
       put_datatypes (fold Symtab.update dt_infos dt_info) |>
       add_cases_induct dt_infos induction' |>
       Theory.parent_path |>
diff -r af605e186480 -r abf0f018b5ec src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -258,7 +258,7 @@
     val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     val thy''' = thy''
       |> (snd o PureThy.add_thmss [(("simps", simps'),
-           [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
+           [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
       |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
       |> Theory.parent_path
   in
diff -r af605e186480 -r abf0f018b5ec src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -11,18 +11,12 @@
   val print_recdefs: theory -> unit
   val get_recdef: theory -> string
     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
-  val simp_add_global: theory attribute
-  val simp_del_global: theory attribute
-  val cong_add_global: theory attribute
-  val cong_del_global: theory attribute
-  val wf_add_global: theory attribute
-  val wf_del_global: theory attribute
-  val simp_add_local: Proof.context attribute
-  val simp_del_local: Proof.context attribute
-  val cong_add_local: Proof.context attribute
-  val cong_del_local: Proof.context attribute
-  val wf_add_local: Proof.context attribute
-  val wf_del_local: Proof.context attribute
+  val simp_add: Context.generic attribute
+  val simp_del: Context.generic attribute
+  val cong_add: Context.generic attribute
+  val cong_del: Context.generic attribute
+  val wf_add: Context.generic attribute
+  val wf_del: Context.generic attribute
   val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
     Attrib.src option -> theory -> theory
       * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
@@ -41,7 +35,6 @@
 structure RecdefPackage: RECDEF_PACKAGE =
 struct
 
-
 val quiet_mode = Tfl.quiet_mode;
 val message = Tfl.message;
 
@@ -152,29 +145,17 @@
 
 (* attributes *)
 
-local
+fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
+  | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
 
-fun global_local f g =
- (fn (thy, thm) => (map_global_hints (f (g thm)) thy, thm),
-  fn (ctxt, thm) => (map_local_hints (f (g thm)) ctxt, thm));
-
-fun mk_attr (add1, add2) (del1, del2) =
- (Attrib.add_del_args add1 del1, Attrib.add_del_args add2 del2);
-
-in
+fun attrib f = Attrib.declaration (map_hints o f);
 
-val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
-val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
-val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
-val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
-val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
-val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
-
-val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
-val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
-val wf_attr = mk_attr (wf_add_global, wf_add_local) (wf_del_global, wf_del_local);
-
-end;
+val simp_add = attrib (map_simps o Drule.add_rule);
+val simp_del = attrib (map_simps o Drule.del_rule);
+val cong_add = attrib (map_congs o add_cong);
+val cong_del = attrib (map_congs o del_cong);
+val wf_add = attrib (map_wfs o Drule.add_rule);
+val wf_del = attrib (map_wfs o Drule.del_rule);
 
 
 (* modifiers *)
@@ -184,15 +165,15 @@
 val recdef_wfN = "recdef_wf";
 
 val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
-  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
-  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
-  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
+  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+  Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
+  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
+  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
+  Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
+  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
+  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
   Clasimp.clasimp_modifiers;
 
 
@@ -243,12 +224,13 @@
                congs wfs name R eqs;
     val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
     val simp_att = if null tcs then
-      [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
+      [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy
       |> Theory.add_path bname
-      |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+      |> PureThy.add_thmss
+        ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> PureThy.add_thms [(("induct", induct), [])];
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
@@ -314,9 +296,12 @@
 val setup =
  [GlobalRecdefData.init, LocalRecdefData.init,
   Attrib.add_attributes
-   [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
-    (recdef_congN, cong_attr, "declaration of recdef cong rule"),
-    (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
+   [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
+      "declaration of recdef simp rule"),
+    (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
+      "declaration of recdef cong rule"),
+    (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
+      "declaration of recdef wf rule")]];
 
 
 (* outer syntax *)
diff -r af605e186480 -r abf0f018b5ec src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -1993,8 +1993,8 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
-           (("iffs",iffs), [iff_add_global])]
+          [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
+           (("iffs",iffs), [Attrib.theory iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme')
       |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
       |> add_record_equalities extension_id equality'
diff -r af605e186480 -r abf0f018b5ec src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -368,7 +368,7 @@
 		("inverts" , inverts ),
 		("injects" , injects ),
 		("copy_rews", copy_rews)])))
-       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
+       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
        |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
                  pat_rews @ dist_les @ dist_eqs @ copy_rews)
 end; (* let *)
diff -r af605e186480 -r abf0f018b5ec src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOLCF/fixrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -250,7 +250,7 @@
       val (simp_thms, thy'') = PureThy.add_thms simps thy';
       
       val simp_names = map (fn name => name^"_simps") cnames;
-      val simp_attribute = rpair [Simplifier.simp_add_global];
+      val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
       val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
     in
       (snd o PureThy.add_thmss simps') thy''
diff -r af605e186480 -r abf0f018b5ec src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/clasimp.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -56,16 +56,12 @@
   val fast_simp_tac: clasimpset -> int -> tactic
   val slow_simp_tac: clasimpset -> int -> tactic
   val best_simp_tac: clasimpset -> int -> tactic
-  val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
-  val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
+  val attrib: (clasimpset * thm list -> clasimpset) -> Context.generic attribute
   val get_local_clasimpset: Proof.context -> clasimpset
   val local_clasimpset_of: Proof.context -> clasimpset
-  val iff_add_global: theory attribute
-  val iff_add_global': theory attribute
-  val iff_del_global: theory attribute
-  val iff_add_local: Proof.context attribute
-  val iff_add_local': Proof.context attribute
-  val iff_del_local: Proof.context attribute
+  val iff_add: Context.generic attribute
+  val iff_add': Context.generic attribute
+  val iff_del: Context.generic attribute
   val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val setup: (theory -> theory) list
@@ -138,18 +134,18 @@
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;
   in
-    (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
-           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
-      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
+    (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]),
+           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS iffD1)))])
+      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS notE))])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;
 
 fun delIff delcs delss ((cs, ss), th) =
   let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
-    (delcs (cs, [zero_rotate (th RS Data.iffD2),
-        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
-      handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
+    (delcs (cs, [zero_rotate (th RS iffD2),
+        Tactic.make_elim (zero_rotate (th RS iffD1))])
+      handle THM _ => (delcs (cs, [zero_rotate (th RS notE)])
         handle THM _ => delcs (cs, [th])),
      delss (ss, [th]))
   end;
@@ -157,10 +153,10 @@
 fun modifier att (x, ths) =
   fst (Thm.applys_attributes [att] (x, rev ths));
 
-fun addXIs which = modifier (which (ContextRules.intro_query NONE));
-fun addXEs which = modifier (which (ContextRules.elim_query NONE));
-fun addXDs which = modifier (which (ContextRules.dest_query NONE));
-fun delXs which = modifier (which ContextRules.rule_del);
+val addXIs = modifier (ContextRules.intro_query NONE);
+val addXEs = modifier (ContextRules.elim_query NONE);
+val addXDs = modifier (ContextRules.dest_query NONE);
+val delXs = modifier ContextRules.rule_del;
 
 in
 
@@ -174,23 +170,11 @@
 fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
 fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
 
-fun addIffs_global (thy, ths) =
-  Library.foldl (addIff
-    (addXEs Attrib.theory, addXIs Attrib.theory)
-    (addXEs Attrib.theory, addXIs Attrib.theory) #1)
-  ((thy, ()), ths) |> #1;
+fun addIffs_generic (x, ths) =
+  Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
 
-fun addIffs_local (ctxt, ths) =
-  Library.foldl (addIff
-    (addXEs Attrib.context, addXIs Attrib.context)
-    (addXEs Attrib.context, addXIs Attrib.context) #1)
-  ((ctxt, ()), ths) |> #1;
-
-fun delIffs_global (thy, ths) =
-  Library.foldl (delIff (delXs Attrib.theory) #1) ((thy, ()), ths) |> #1;
-
-fun delIffs_local (ctxt, ths) =
-  Library.foldl (delIff (delXs Attrib.context) #1) ((ctxt, ()), ths) |> #1;
+fun delIffs_generic (x, ths) =
+  Library.foldl (delIff delXs #1) ((x, ()), ths) |> #1;
 
 end;
 
@@ -272,20 +256,6 @@
 
 (* access clasimpset *)
 
-fun change_global_css f (thy, th) =
-  (change_clasimpset_of thy (fn css => f (css, [th])); (thy, th));
-
-fun change_local_css f (ctxt, th) =
-  let
-    val cs = Classical.get_local_claset ctxt;
-    val ss = Simplifier.get_local_simpset ctxt;
-    val (cs', ss') = f ((cs, ss), [th]);
-    val ctxt' =
-      ctxt
-      |> Classical.put_local_claset cs'
-      |> Simplifier.put_local_simpset ss';
-  in (ctxt', th) end;
-
 fun get_local_clasimpset ctxt =
   (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
 
@@ -295,23 +265,29 @@
 
 (* attributes *)
 
-fun change_rules f (x, th) = (f (x, [th]), th);
-
-val iff_add_global = change_global_css (op addIffs);
-val iff_add_global' = change_rules addIffs_global;
-val iff_del_global = change_global_css (op delIffs) o change_rules delIffs_global;
-val iff_add_local = change_local_css (op addIffs);
-val iff_add_local' = change_rules addIffs_local;
-val iff_del_local = change_local_css (op delIffs) o change_rules delIffs_local;
+fun attrib f = Attrib.declaration (fn th =>
+ fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
+  | Context.Proof ctxt =>
+      let
+        val cs = Classical.get_local_claset ctxt;
+        val ss = Simplifier.get_local_simpset ctxt;
+        val (cs', ss') = f ((cs, ss), [th]);
+        val ctxt' =
+          ctxt
+          |> Classical.put_local_claset cs'
+          |> Simplifier.put_local_simpset ss';
+      in Context.Proof ctxt' end);
 
-fun iff_att add add' del = Attrib.syntax (Scan.lift
- (Args.del >> K del ||
-  Scan.option Args.add -- Args.query >> K add' ||
-  Scan.option Args.add >> K add));
+fun attrib' f (x, th) = (f (x, [th]), th);
 
-val iff_attr =
- (iff_att iff_add_global iff_add_global' iff_del_global,
-  iff_att iff_add_local iff_add_local' iff_del_local);
+val iff_add = attrib (op addIffs);
+val iff_add' = attrib' addIffs_generic;
+val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
+
+val iff_att = Attrib.syntax (Scan.lift
+ (Args.del >> K iff_del ||
+  Scan.option Args.add -- Args.query >> K iff_add' ||
+  Scan.option Args.add >> K iff_add));
 
 
 (* method modifiers *)
@@ -319,9 +295,10 @@
 val iffN = "iff";
 
 val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add_local): Method.modifier),
-  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add_local'),
-  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del_local)];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon
+    >> K ((I, Attrib.context iff_add): Method.modifier),
+  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, Attrib.context iff_add'),
+  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, Attrib.context iff_del)];
 
 val clasimp_modifiers =
   Simplifier.simp_modifiers @ Splitter.split_modifiers @
@@ -351,7 +328,7 @@
 
 val setup =
  [Attrib.add_attributes
-  [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
+  [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")],
   Method.add_methods
    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
diff -r af605e186480 -r abf0f018b5ec src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/classical.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -143,20 +143,13 @@
   val print_local_claset: Proof.context -> unit
   val get_local_claset: Proof.context -> claset
   val put_local_claset: claset -> Proof.context -> Proof.context
-  val safe_dest_global: theory attribute
-  val safe_elim_global: theory attribute
-  val safe_intro_global: theory attribute
-  val haz_dest_global: theory attribute
-  val haz_elim_global: theory attribute
-  val haz_intro_global: theory attribute
-  val rule_del_global: theory attribute
-  val safe_dest_local: Proof.context attribute
-  val safe_elim_local: Proof.context attribute
-  val safe_intro_local: Proof.context attribute
-  val haz_dest_local: Proof.context attribute
-  val haz_elim_local: Proof.context attribute
-  val haz_intro_local: Proof.context attribute
-  val rule_del_local: Proof.context attribute
+  val safe_dest: Context.generic attribute
+  val safe_elim: Context.generic attribute
+  val safe_intro: Context.generic attribute
+  val haz_dest: Context.generic attribute
+  val haz_elim: Context.generic attribute
+  val haz_intro: Context.generic attribute
+  val rule_del: Context.generic attribute
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
@@ -959,24 +952,17 @@
 
 (* attributes *)
 
-fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th));
-fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th);
+fun attrib f = Attrib.declaration (fn th =>
+   fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy)
+    | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt));
 
-val safe_dest_global = change_global_cs (op addSDs);
-val safe_elim_global = change_global_cs (op addSEs);
-val safe_intro_global = change_global_cs (op addSIs);
-val haz_dest_global = change_global_cs (op addDs);
-val haz_elim_global = change_global_cs (op addEs);
-val haz_intro_global = change_global_cs (op addIs);
-val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
-
-val safe_dest_local = change_local_cs (op addSDs);
-val safe_elim_local = change_local_cs (op addSEs);
-val safe_intro_local = change_local_cs (op addSIs);
-val haz_dest_local = change_local_cs (op addDs);
-val haz_elim_local = change_local_cs (op addEs);
-val haz_intro_local = change_local_cs (op addIs);
-val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
+val safe_dest = attrib (op addSDs);
+val safe_elim = attrib (op addSEs);
+val safe_intro = attrib (op addSIs);
+val haz_dest = attrib (op addDs);
+val haz_elim = attrib (op addEs);
+val haz_intro = attrib (op addIs);
+val rule_del = attrib (op delrules) o ContextRules.rule_del;
 
 
 (* tactics referring to the implicit claset *)
@@ -1018,19 +1004,13 @@
 
 val setup_attrs = Attrib.add_attributes
  [("swapped", (swapped, swapped), "classical swap of introduction rule"),
-  (destN,
-   (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
-    add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
-    "declaration of destruction rule"),
-  (elimN,
-   (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
-    add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
-    "declaration of elimination rule"),
-  (introN,
-   (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
-    add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
-    "declaration of introduction rule"),
-  (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
+  (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest),
+    "declaration of Classical destruction rule"),
+  (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim),
+    "declaration of Classical elimination rule"),
+  (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro),
+    "declaration of Classical introduction rule"),
+  (ruleN, Attrib.common (del_rule rule_del),
     "remove declaration of intro/elim/dest rule")];
 
 
@@ -1078,13 +1058,13 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier),
-  Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
-  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
-  Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
-  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
-  Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
-  Args.del -- Args.colon >> K (I, rule_del_local)];
+ [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier),
+  Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest),
+  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim),
+  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim),
+  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro),
+  Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro),
+  Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
 
 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
diff -r af605e186480 -r abf0f018b5ec src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/splitter.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -32,10 +32,8 @@
   val delsplits       : simpset * thm list -> simpset
   val Addsplits       : thm list -> unit
   val Delsplits       : thm list -> unit
-  val split_add_global: theory attribute
-  val split_del_global: theory attribute
-  val split_add_local: Proof.context attribute
-  val split_del_local: Proof.context attribute
+  val split_add: Context.generic attribute
+  val split_del: Context.generic attribute
   val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
   val setup: (theory -> theory) list
 end;
@@ -405,6 +403,7 @@
          gen_split_tac splits
       end;
 
+
 (** declare split rules **)
 
 (* addsplits / delsplits *)
@@ -437,33 +436,28 @@
 
 val splitN = "split";
 
-val split_add_global = Simplifier.change_global_ss (op addsplits);
-val split_del_global = Simplifier.change_global_ss (op delsplits);
-val split_add_local = Simplifier.change_local_ss (op addsplits);
-val split_del_local = Simplifier.change_local_ss (op delsplits);
-
-val split_attr =
- (Attrib.add_del_args split_add_global split_del_global,
-  Attrib.add_del_args split_add_local split_del_local);
+val split_add = Simplifier.attrib (op addsplits);
+val split_del = Simplifier.attrib (op delsplits);
 
 
 (* methods *)
 
 val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
+ [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
+  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
+  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
 
-val split_args = #2 oo Method.syntax Attrib.local_thms;
-
-fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
+fun split_meth src =
+  Method.syntax Attrib.local_thms src
+  #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
 
 
-
-(** theory setup **)
+(* theory setup *)
 
 val setup =
- [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
-  Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
+ [Attrib.add_attributes
+  [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
+    "declaration of case split rule")],
+  Method.add_methods [(splitN, split_meth, "apply case split rule")]];
 
 end;
diff -r af605e186480 -r abf0f018b5ec src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Pure/simplifier.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -64,16 +64,11 @@
   val print_local_simpset: Proof.context -> unit
   val get_local_simpset: Proof.context -> simpset
   val put_local_simpset: simpset -> Proof.context -> Proof.context
-  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
-  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
-  val simp_add_global: theory attribute
-  val simp_del_global: theory attribute
-  val simp_add_local: Proof.context attribute
-  val simp_del_local: Proof.context attribute
-  val cong_add_global: theory attribute
-  val cong_del_global: theory attribute
-  val cong_add_local: Proof.context attribute
-  val cong_del_local: Proof.context attribute
+  val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
+  val simp_add: Context.generic attribute
+  val simp_del: Context.generic attribute
+  val cong_add: Context.generic attribute
+  val cong_del: Context.generic attribute
   val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
@@ -143,18 +138,14 @@
 
 (* attributes *)
 
-fun change_global_ss f (thy, th) = (change_simpset_of thy (fn ss => f (ss, [th])); (thy, th));
-fun change_local_ss f (ctxt, th) = (LocalSimpset.map (fn ss => f (ss, [th])) ctxt, th);
+fun attrib f = Attrib.declaration (fn th =>
+   fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
+    | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
 
-val simp_add_global = change_global_ss (op addsimps);
-val simp_del_global = change_global_ss (op delsimps);
-val simp_add_local = change_local_ss (op addsimps);
-val simp_del_local = change_local_ss (op delsimps);
-
-val cong_add_global = change_global_ss (op addcongs);
-val cong_del_global = change_global_ss (op delcongs);
-val cong_add_local = change_local_ss (op addcongs);
-val cong_del_local = change_local_ss (op delcongs);
+val simp_add = attrib (op addsimps);
+val simp_del = attrib (op delsimps);
+val cong_add = attrib (op addcongs);
+val cong_del = attrib (op delcongs);
 
 
 
@@ -243,14 +234,6 @@
 val no_asm_simpN = "no_asm_simp";
 val asm_lrN = "asm_lr";
 
-val simp_attr =
- (Attrib.add_del_args simp_add_global simp_del_global,
-  Attrib.add_del_args simp_add_local simp_del_local);
-
-val cong_attr =
- (Attrib.add_del_args cong_add_global cong_del_global,
-  Attrib.add_del_args cong_add_local cong_del_local);
-
 
 (* conversions *)
 
@@ -262,15 +245,14 @@
     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
     Scan.succeed asm_full_simplify) |> Scan.lift) x;
 
-fun simplified_att get args =
-  Attrib.syntax (conv_mode -- args >> (fn (f, ths) => Attrib.rule (fn x =>
-    f ((if null ths then I else MetaSimplifier.clear_ss) (get x) addsimps ths))));
+fun get_ss (Context.Theory thy) = simpset_of thy
+  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
 
 in
 
-val simplified_attr =
- (simplified_att simpset_of Attrib.global_thmss,
-  simplified_att local_simpset_of Attrib.local_thmss);
+val simplified =
+  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
+    f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
 
 end;
 
@@ -279,9 +261,11 @@
 
 val _ = Context.add_setup
  [Attrib.add_attributes
-   [(simpN, simp_attr, "declaration of simplification rule"),
-    (congN, cong_attr, "declaration of Simplifier congruence rule"),
-    ("simplified", simplified_attr, "simplified rule")]];
+   [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
+      "declaration of Simplifier rule"),
+    (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
+      "declaration of Simplifier congruence rule"),
+    ("simplified", Attrib.common simplified, "simplified rule")]];
 
 
 
@@ -302,22 +286,23 @@
   >> (curry (Library.foldl op o) I o rev)) x;
 
 val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local): Method.modifier),
-  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
+ [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
+  Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
+  Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
 
 val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
+ [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
+  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
-    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
+    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, simp_add_local),
-  Args.del -- Args.colon >> K (I, simp_del_local),
-  Args.$$$ onlyN -- Args.colon >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
+ [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+  Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+  Args.$$$ onlyN -- Args.colon
+    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
    @ cong_modifiers;
 
 fun simp_args more_mods =
diff -r af605e186480 -r abf0f018b5ec src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -367,8 +367,8 @@
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Theory.add_path big_rec_base_name
         |> PureThy.add_thmss
-         [(("simps", simps), [Simplifier.simp_add_global]),
-          (("", intrs), [Classical.safe_intro_global]),
+         [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
+          (("", intrs), [Attrib.theory Classical.safe_intro]),
           (("con_defs", con_defs), []),
           (("case_eqns", case_eqns), []),
           (("recursor_eqns", recursor_eqns), []),
diff -r af605e186480 -r abf0f018b5ec src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -165,7 +165,7 @@
   in
     thy
     |> Theory.add_path (Sign.base_name big_rec_name)
-    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
+    |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
     |> Theory.parent_path
diff -r af605e186480 -r abf0f018b5ec src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -191,7 +191,7 @@
       |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
     val (_, thy3) =
       thy2
-      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]
+      |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])]
       ||> Theory.parent_path;
   in (thy3, eqn_thms') end;