generic attributes;
authorwenzelm
Sat Jan 14 22:25:34 2006 +0100 (2006-01-14 ago)
changeset 18688abf0f018b5ec
parent 18687 af605e186480
child 18689 a50587cd8414
generic attributes;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/simplifier.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -350,10 +350,10 @@
     1.4                    weak_case_congs cong_att =
     1.5    (snd o PureThy.add_thmss [(("simps", simps), []),
     1.6      (("", List.concat case_thms @ size_thms @ 
     1.7 -          List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
     1.8 +          List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
     1.9      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    1.10 -    (("", List.concat inject),               [iff_add_global]),
    1.11 -    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim_global]),
    1.12 +    (("", List.concat inject),               [Attrib.theory iff_add]),
    1.13 +    (("", map name_notE (List.concat distinct)),  [Attrib.theory Classical.safe_elim]),
    1.14      (("", weak_case_congs),                  [cong_att])]);
    1.15  
    1.16  
    1.17 @@ -747,7 +747,7 @@
    1.18        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
    1.19        |> Theory.add_path (space_implode "_" new_type_names)
    1.20        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.21 -           weak_case_congs Simplifier.cong_add_global
    1.22 +           weak_case_congs (Attrib.theory Simplifier.cong_add)
    1.23        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.24        |> add_cases_induct dt_infos induct
    1.25        |> Theory.parent_path
    1.26 @@ -806,7 +806,7 @@
    1.27        |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
    1.28        |> Theory.add_path (space_implode "_" new_type_names)
    1.29        |> add_rules simps case_thms size_thms rec_thms inject distinct
    1.30 -            weak_case_congs (Simplifier.change_global_ss (op addcongs))
    1.31 +            weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
    1.32        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    1.33        |> add_cases_induct dt_infos induct
    1.34        |> Theory.parent_path
    1.35 @@ -913,7 +913,7 @@
    1.36      val thy11 = thy10 |>
    1.37        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.38        add_rules simps case_thms size_thms rec_thms inject distinct
    1.39 -                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.40 +                weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |> 
    1.41        put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.42        add_cases_induct dt_infos induction' |>
    1.43        Theory.parent_path |>
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
     2.3 @@ -258,7 +258,7 @@
     2.4      val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     2.5      val thy''' = thy''
     2.6        |> (snd o PureThy.add_thmss [(("simps", simps'),
     2.7 -           [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
     2.8 +           [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
     2.9        |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    2.10        |> Theory.parent_path
    2.11    in
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Jan 14 17:20:51 2006 +0100
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Jan 14 22:25:34 2006 +0100
     3.3 @@ -11,18 +11,12 @@
     3.4    val print_recdefs: theory -> unit
     3.5    val get_recdef: theory -> string
     3.6      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     3.7 -  val simp_add_global: theory attribute
     3.8 -  val simp_del_global: theory attribute
     3.9 -  val cong_add_global: theory attribute
    3.10 -  val cong_del_global: theory attribute
    3.11 -  val wf_add_global: theory attribute
    3.12 -  val wf_del_global: theory attribute
    3.13 -  val simp_add_local: Proof.context attribute
    3.14 -  val simp_del_local: Proof.context attribute
    3.15 -  val cong_add_local: Proof.context attribute
    3.16 -  val cong_del_local: Proof.context attribute
    3.17 -  val wf_add_local: Proof.context attribute
    3.18 -  val wf_del_local: Proof.context attribute
    3.19 +  val simp_add: Context.generic attribute
    3.20 +  val simp_del: Context.generic attribute
    3.21 +  val cong_add: Context.generic attribute
    3.22 +  val cong_del: Context.generic attribute
    3.23 +  val wf_add: Context.generic attribute
    3.24 +  val wf_del: Context.generic attribute
    3.25    val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
    3.26      Attrib.src option -> theory -> theory
    3.27        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    3.28 @@ -41,7 +35,6 @@
    3.29  structure RecdefPackage: RECDEF_PACKAGE =
    3.30  struct
    3.31  
    3.32 -
    3.33  val quiet_mode = Tfl.quiet_mode;
    3.34  val message = Tfl.message;
    3.35  
    3.36 @@ -152,29 +145,17 @@
    3.37  
    3.38  (* attributes *)
    3.39  
    3.40 -local
    3.41 +fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
    3.42 +  | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
    3.43  
    3.44 -fun global_local f g =
    3.45 - (fn (thy, thm) => (map_global_hints (f (g thm)) thy, thm),
    3.46 -  fn (ctxt, thm) => (map_local_hints (f (g thm)) ctxt, thm));
    3.47 -
    3.48 -fun mk_attr (add1, add2) (del1, del2) =
    3.49 - (Attrib.add_del_args add1 del1, Attrib.add_del_args add2 del2);
    3.50 -
    3.51 -in
    3.52 +fun attrib f = Attrib.declaration (map_hints o f);
    3.53  
    3.54 -val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
    3.55 -val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
    3.56 -val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
    3.57 -val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
    3.58 -val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
    3.59 -val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
    3.60 -
    3.61 -val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
    3.62 -val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
    3.63 -val wf_attr = mk_attr (wf_add_global, wf_add_local) (wf_del_global, wf_del_local);
    3.64 -
    3.65 -end;
    3.66 +val simp_add = attrib (map_simps o Drule.add_rule);
    3.67 +val simp_del = attrib (map_simps o Drule.del_rule);
    3.68 +val cong_add = attrib (map_congs o add_cong);
    3.69 +val cong_del = attrib (map_congs o del_cong);
    3.70 +val wf_add = attrib (map_wfs o Drule.add_rule);
    3.71 +val wf_del = attrib (map_wfs o Drule.del_rule);
    3.72  
    3.73  
    3.74  (* modifiers *)
    3.75 @@ -184,15 +165,15 @@
    3.76  val recdef_wfN = "recdef_wf";
    3.77  
    3.78  val recdef_modifiers =
    3.79 - [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
    3.80 -  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
    3.81 -  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
    3.82 -  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
    3.83 -  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
    3.84 -  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
    3.85 -  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
    3.86 -  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
    3.87 -  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
    3.88 + [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
    3.89 +  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
    3.90 +  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
    3.91 +  Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
    3.92 +  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
    3.93 +  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
    3.94 +  Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
    3.95 +  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
    3.96 +  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
    3.97    Clasimp.clasimp_modifiers;
    3.98  
    3.99  
   3.100 @@ -243,12 +224,13 @@
   3.101                 congs wfs name R eqs;
   3.102      val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
   3.103      val simp_att = if null tcs then
   3.104 -      [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
   3.105 +      [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
   3.106  
   3.107      val ((simps' :: rules', [induct']), thy) =
   3.108        thy
   3.109        |> Theory.add_path bname
   3.110 -      |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   3.111 +      |> PureThy.add_thmss
   3.112 +        ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   3.113        ||>> PureThy.add_thms [(("induct", induct), [])];
   3.114      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   3.115      val thy =
   3.116 @@ -314,9 +296,12 @@
   3.117  val setup =
   3.118   [GlobalRecdefData.init, LocalRecdefData.init,
   3.119    Attrib.add_attributes
   3.120 -   [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
   3.121 -    (recdef_congN, cong_attr, "declaration of recdef cong rule"),
   3.122 -    (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
   3.123 +   [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   3.124 +      "declaration of recdef simp rule"),
   3.125 +    (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   3.126 +      "declaration of recdef cong rule"),
   3.127 +    (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
   3.128 +      "declaration of recdef wf rule")]];
   3.129  
   3.130  
   3.131  (* outer syntax *)
     4.1 --- a/src/HOL/Tools/record_package.ML	Sat Jan 14 17:20:51 2006 +0100
     4.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jan 14 22:25:34 2006 +0100
     4.3 @@ -1993,8 +1993,8 @@
     4.4      val final_thy =
     4.5        thms_thy
     4.6        |> (snd oo PureThy.add_thmss)
     4.7 -          [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
     4.8 -           (("iffs",iffs), [iff_add_global])]
     4.9 +          [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
    4.10 +           (("iffs",iffs), [Attrib.theory iff_add])]
    4.11        |> put_record name (make_record_info args parent fields extension induct_scheme')
    4.12        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
    4.13        |> add_record_equalities extension_id equality'
     5.1 --- a/src/HOLCF/domain/theorems.ML	Sat Jan 14 17:20:51 2006 +0100
     5.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jan 14 22:25:34 2006 +0100
     5.3 @@ -368,7 +368,7 @@
     5.4  		("inverts" , inverts ),
     5.5  		("injects" , injects ),
     5.6  		("copy_rews", copy_rews)])))
     5.7 -       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
     5.8 +       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
     5.9         |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
    5.10                   pat_rews @ dist_les @ dist_eqs @ copy_rews)
    5.11  end; (* let *)
     6.1 --- a/src/HOLCF/fixrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
     6.2 +++ b/src/HOLCF/fixrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
     6.3 @@ -250,7 +250,7 @@
     6.4        val (simp_thms, thy'') = PureThy.add_thms simps thy';
     6.5        
     6.6        val simp_names = map (fn name => name^"_simps") cnames;
     6.7 -      val simp_attribute = rpair [Simplifier.simp_add_global];
     6.8 +      val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
     6.9        val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
    6.10      in
    6.11        (snd o PureThy.add_thmss simps') thy''
     7.1 --- a/src/Provers/clasimp.ML	Sat Jan 14 17:20:51 2006 +0100
     7.2 +++ b/src/Provers/clasimp.ML	Sat Jan 14 22:25:34 2006 +0100
     7.3 @@ -56,16 +56,12 @@
     7.4    val fast_simp_tac: clasimpset -> int -> tactic
     7.5    val slow_simp_tac: clasimpset -> int -> tactic
     7.6    val best_simp_tac: clasimpset -> int -> tactic
     7.7 -  val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
     7.8 -  val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
     7.9 +  val attrib: (clasimpset * thm list -> clasimpset) -> Context.generic attribute
    7.10    val get_local_clasimpset: Proof.context -> clasimpset
    7.11    val local_clasimpset_of: Proof.context -> clasimpset
    7.12 -  val iff_add_global: theory attribute
    7.13 -  val iff_add_global': theory attribute
    7.14 -  val iff_del_global: theory attribute
    7.15 -  val iff_add_local: Proof.context attribute
    7.16 -  val iff_add_local': Proof.context attribute
    7.17 -  val iff_del_local: Proof.context attribute
    7.18 +  val iff_add: Context.generic attribute
    7.19 +  val iff_add': Context.generic attribute
    7.20 +  val iff_del: Context.generic attribute
    7.21    val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    7.22    val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    7.23    val setup: (theory -> theory) list
    7.24 @@ -138,18 +134,18 @@
    7.25      val (elim, intro) = if n = 0 then decls1 else decls2;
    7.26      val zero_rotate = zero_var_indexes o rotate_prems n;
    7.27    in
    7.28 -    (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
    7.29 -           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
    7.30 -      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
    7.31 +    (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]),
    7.32 +           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS iffD1)))])
    7.33 +      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS notE))])
    7.34          handle THM _ => intro (cs, [th])),
    7.35       simp (ss, [th]))
    7.36    end;
    7.37  
    7.38  fun delIff delcs delss ((cs, ss), th) =
    7.39    let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    7.40 -    (delcs (cs, [zero_rotate (th RS Data.iffD2),
    7.41 -        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
    7.42 -      handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
    7.43 +    (delcs (cs, [zero_rotate (th RS iffD2),
    7.44 +        Tactic.make_elim (zero_rotate (th RS iffD1))])
    7.45 +      handle THM _ => (delcs (cs, [zero_rotate (th RS notE)])
    7.46          handle THM _ => delcs (cs, [th])),
    7.47       delss (ss, [th]))
    7.48    end;
    7.49 @@ -157,10 +153,10 @@
    7.50  fun modifier att (x, ths) =
    7.51    fst (Thm.applys_attributes [att] (x, rev ths));
    7.52  
    7.53 -fun addXIs which = modifier (which (ContextRules.intro_query NONE));
    7.54 -fun addXEs which = modifier (which (ContextRules.elim_query NONE));
    7.55 -fun addXDs which = modifier (which (ContextRules.dest_query NONE));
    7.56 -fun delXs which = modifier (which ContextRules.rule_del);
    7.57 +val addXIs = modifier (ContextRules.intro_query NONE);
    7.58 +val addXEs = modifier (ContextRules.elim_query NONE);
    7.59 +val addXDs = modifier (ContextRules.dest_query NONE);
    7.60 +val delXs = modifier ContextRules.rule_del;
    7.61  
    7.62  in
    7.63  
    7.64 @@ -174,23 +170,11 @@
    7.65  fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
    7.66  fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
    7.67  
    7.68 -fun addIffs_global (thy, ths) =
    7.69 -  Library.foldl (addIff
    7.70 -    (addXEs Attrib.theory, addXIs Attrib.theory)
    7.71 -    (addXEs Attrib.theory, addXIs Attrib.theory) #1)
    7.72 -  ((thy, ()), ths) |> #1;
    7.73 +fun addIffs_generic (x, ths) =
    7.74 +  Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
    7.75  
    7.76 -fun addIffs_local (ctxt, ths) =
    7.77 -  Library.foldl (addIff
    7.78 -    (addXEs Attrib.context, addXIs Attrib.context)
    7.79 -    (addXEs Attrib.context, addXIs Attrib.context) #1)
    7.80 -  ((ctxt, ()), ths) |> #1;
    7.81 -
    7.82 -fun delIffs_global (thy, ths) =
    7.83 -  Library.foldl (delIff (delXs Attrib.theory) #1) ((thy, ()), ths) |> #1;
    7.84 -
    7.85 -fun delIffs_local (ctxt, ths) =
    7.86 -  Library.foldl (delIff (delXs Attrib.context) #1) ((ctxt, ()), ths) |> #1;
    7.87 +fun delIffs_generic (x, ths) =
    7.88 +  Library.foldl (delIff delXs #1) ((x, ()), ths) |> #1;
    7.89  
    7.90  end;
    7.91  
    7.92 @@ -272,20 +256,6 @@
    7.93  
    7.94  (* access clasimpset *)
    7.95  
    7.96 -fun change_global_css f (thy, th) =
    7.97 -  (change_clasimpset_of thy (fn css => f (css, [th])); (thy, th));
    7.98 -
    7.99 -fun change_local_css f (ctxt, th) =
   7.100 -  let
   7.101 -    val cs = Classical.get_local_claset ctxt;
   7.102 -    val ss = Simplifier.get_local_simpset ctxt;
   7.103 -    val (cs', ss') = f ((cs, ss), [th]);
   7.104 -    val ctxt' =
   7.105 -      ctxt
   7.106 -      |> Classical.put_local_claset cs'
   7.107 -      |> Simplifier.put_local_simpset ss';
   7.108 -  in (ctxt', th) end;
   7.109 -
   7.110  fun get_local_clasimpset ctxt =
   7.111    (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   7.112  
   7.113 @@ -295,23 +265,29 @@
   7.114  
   7.115  (* attributes *)
   7.116  
   7.117 -fun change_rules f (x, th) = (f (x, [th]), th);
   7.118 -
   7.119 -val iff_add_global = change_global_css (op addIffs);
   7.120 -val iff_add_global' = change_rules addIffs_global;
   7.121 -val iff_del_global = change_global_css (op delIffs) o change_rules delIffs_global;
   7.122 -val iff_add_local = change_local_css (op addIffs);
   7.123 -val iff_add_local' = change_rules addIffs_local;
   7.124 -val iff_del_local = change_local_css (op delIffs) o change_rules delIffs_local;
   7.125 +fun attrib f = Attrib.declaration (fn th =>
   7.126 + fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
   7.127 +  | Context.Proof ctxt =>
   7.128 +      let
   7.129 +        val cs = Classical.get_local_claset ctxt;
   7.130 +        val ss = Simplifier.get_local_simpset ctxt;
   7.131 +        val (cs', ss') = f ((cs, ss), [th]);
   7.132 +        val ctxt' =
   7.133 +          ctxt
   7.134 +          |> Classical.put_local_claset cs'
   7.135 +          |> Simplifier.put_local_simpset ss';
   7.136 +      in Context.Proof ctxt' end);
   7.137  
   7.138 -fun iff_att add add' del = Attrib.syntax (Scan.lift
   7.139 - (Args.del >> K del ||
   7.140 -  Scan.option Args.add -- Args.query >> K add' ||
   7.141 -  Scan.option Args.add >> K add));
   7.142 +fun attrib' f (x, th) = (f (x, [th]), th);
   7.143  
   7.144 -val iff_attr =
   7.145 - (iff_att iff_add_global iff_add_global' iff_del_global,
   7.146 -  iff_att iff_add_local iff_add_local' iff_del_local);
   7.147 +val iff_add = attrib (op addIffs);
   7.148 +val iff_add' = attrib' addIffs_generic;
   7.149 +val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
   7.150 +
   7.151 +val iff_att = Attrib.syntax (Scan.lift
   7.152 + (Args.del >> K iff_del ||
   7.153 +  Scan.option Args.add -- Args.query >> K iff_add' ||
   7.154 +  Scan.option Args.add >> K iff_add));
   7.155  
   7.156  
   7.157  (* method modifiers *)
   7.158 @@ -319,9 +295,10 @@
   7.159  val iffN = "iff";
   7.160  
   7.161  val iff_modifiers =
   7.162 - [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add_local): Method.modifier),
   7.163 -  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add_local'),
   7.164 -  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del_local)];
   7.165 + [Args.$$$ iffN -- Scan.option Args.add -- Args.colon
   7.166 +    >> K ((I, Attrib.context iff_add): Method.modifier),
   7.167 +  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, Attrib.context iff_add'),
   7.168 +  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, Attrib.context iff_del)];
   7.169  
   7.170  val clasimp_modifiers =
   7.171    Simplifier.simp_modifiers @ Splitter.split_modifiers @
   7.172 @@ -351,7 +328,7 @@
   7.173  
   7.174  val setup =
   7.175   [Attrib.add_attributes
   7.176 -  [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
   7.177 +  [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")],
   7.178    Method.add_methods
   7.179     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   7.180      ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
     8.1 --- a/src/Provers/classical.ML	Sat Jan 14 17:20:51 2006 +0100
     8.2 +++ b/src/Provers/classical.ML	Sat Jan 14 22:25:34 2006 +0100
     8.3 @@ -143,20 +143,13 @@
     8.4    val print_local_claset: Proof.context -> unit
     8.5    val get_local_claset: Proof.context -> claset
     8.6    val put_local_claset: claset -> Proof.context -> Proof.context
     8.7 -  val safe_dest_global: theory attribute
     8.8 -  val safe_elim_global: theory attribute
     8.9 -  val safe_intro_global: theory attribute
    8.10 -  val haz_dest_global: theory attribute
    8.11 -  val haz_elim_global: theory attribute
    8.12 -  val haz_intro_global: theory attribute
    8.13 -  val rule_del_global: theory attribute
    8.14 -  val safe_dest_local: Proof.context attribute
    8.15 -  val safe_elim_local: Proof.context attribute
    8.16 -  val safe_intro_local: Proof.context attribute
    8.17 -  val haz_dest_local: Proof.context attribute
    8.18 -  val haz_elim_local: Proof.context attribute
    8.19 -  val haz_intro_local: Proof.context attribute
    8.20 -  val rule_del_local: Proof.context attribute
    8.21 +  val safe_dest: Context.generic attribute
    8.22 +  val safe_elim: Context.generic attribute
    8.23 +  val safe_intro: Context.generic attribute
    8.24 +  val haz_dest: Context.generic attribute
    8.25 +  val haz_elim: Context.generic attribute
    8.26 +  val haz_intro: Context.generic attribute
    8.27 +  val rule_del: Context.generic attribute
    8.28    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    8.29    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    8.30    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    8.31 @@ -959,24 +952,17 @@
    8.32  
    8.33  (* attributes *)
    8.34  
    8.35 -fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th));
    8.36 -fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th);
    8.37 +fun attrib f = Attrib.declaration (fn th =>
    8.38 +   fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy)
    8.39 +    | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt));
    8.40  
    8.41 -val safe_dest_global = change_global_cs (op addSDs);
    8.42 -val safe_elim_global = change_global_cs (op addSEs);
    8.43 -val safe_intro_global = change_global_cs (op addSIs);
    8.44 -val haz_dest_global = change_global_cs (op addDs);
    8.45 -val haz_elim_global = change_global_cs (op addEs);
    8.46 -val haz_intro_global = change_global_cs (op addIs);
    8.47 -val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
    8.48 -
    8.49 -val safe_dest_local = change_local_cs (op addSDs);
    8.50 -val safe_elim_local = change_local_cs (op addSEs);
    8.51 -val safe_intro_local = change_local_cs (op addSIs);
    8.52 -val haz_dest_local = change_local_cs (op addDs);
    8.53 -val haz_elim_local = change_local_cs (op addEs);
    8.54 -val haz_intro_local = change_local_cs (op addIs);
    8.55 -val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
    8.56 +val safe_dest = attrib (op addSDs);
    8.57 +val safe_elim = attrib (op addSEs);
    8.58 +val safe_intro = attrib (op addSIs);
    8.59 +val haz_dest = attrib (op addDs);
    8.60 +val haz_elim = attrib (op addEs);
    8.61 +val haz_intro = attrib (op addIs);
    8.62 +val rule_del = attrib (op delrules) o ContextRules.rule_del;
    8.63  
    8.64  
    8.65  (* tactics referring to the implicit claset *)
    8.66 @@ -1018,19 +1004,13 @@
    8.67  
    8.68  val setup_attrs = Attrib.add_attributes
    8.69   [("swapped", (swapped, swapped), "classical swap of introduction rule"),
    8.70 -  (destN,
    8.71 -   (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
    8.72 -    add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
    8.73 -    "declaration of destruction rule"),
    8.74 -  (elimN,
    8.75 -   (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
    8.76 -    add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
    8.77 -    "declaration of elimination rule"),
    8.78 -  (introN,
    8.79 -   (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
    8.80 -    add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
    8.81 -    "declaration of introduction rule"),
    8.82 -  (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
    8.83 +  (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest),
    8.84 +    "declaration of Classical destruction rule"),
    8.85 +  (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim),
    8.86 +    "declaration of Classical elimination rule"),
    8.87 +  (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro),
    8.88 +    "declaration of Classical introduction rule"),
    8.89 +  (ruleN, Attrib.common (del_rule rule_del),
    8.90      "remove declaration of intro/elim/dest rule")];
    8.91  
    8.92  
    8.93 @@ -1078,13 +1058,13 @@
    8.94  (* automatic methods *)
    8.95  
    8.96  val cla_modifiers =
    8.97 - [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier),
    8.98 -  Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
    8.99 -  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
   8.100 -  Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
   8.101 -  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
   8.102 -  Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
   8.103 -  Args.del -- Args.colon >> K (I, rule_del_local)];
   8.104 + [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier),
   8.105 +  Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest),
   8.106 +  Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim),
   8.107 +  Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim),
   8.108 +  Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro),
   8.109 +  Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro),
   8.110 +  Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
   8.111  
   8.112  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   8.113    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
     9.1 --- a/src/Provers/splitter.ML	Sat Jan 14 17:20:51 2006 +0100
     9.2 +++ b/src/Provers/splitter.ML	Sat Jan 14 22:25:34 2006 +0100
     9.3 @@ -32,10 +32,8 @@
     9.4    val delsplits       : simpset * thm list -> simpset
     9.5    val Addsplits       : thm list -> unit
     9.6    val Delsplits       : thm list -> unit
     9.7 -  val split_add_global: theory attribute
     9.8 -  val split_del_global: theory attribute
     9.9 -  val split_add_local: Proof.context attribute
    9.10 -  val split_del_local: Proof.context attribute
    9.11 +  val split_add: Context.generic attribute
    9.12 +  val split_del: Context.generic attribute
    9.13    val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
    9.14    val setup: (theory -> theory) list
    9.15  end;
    9.16 @@ -405,6 +403,7 @@
    9.17           gen_split_tac splits
    9.18        end;
    9.19  
    9.20 +
    9.21  (** declare split rules **)
    9.22  
    9.23  (* addsplits / delsplits *)
    9.24 @@ -437,33 +436,28 @@
    9.25  
    9.26  val splitN = "split";
    9.27  
    9.28 -val split_add_global = Simplifier.change_global_ss (op addsplits);
    9.29 -val split_del_global = Simplifier.change_global_ss (op delsplits);
    9.30 -val split_add_local = Simplifier.change_local_ss (op addsplits);
    9.31 -val split_del_local = Simplifier.change_local_ss (op delsplits);
    9.32 -
    9.33 -val split_attr =
    9.34 - (Attrib.add_del_args split_add_global split_del_global,
    9.35 -  Attrib.add_del_args split_add_local split_del_local);
    9.36 +val split_add = Simplifier.attrib (op addsplits);
    9.37 +val split_del = Simplifier.attrib (op delsplits);
    9.38  
    9.39  
    9.40  (* methods *)
    9.41  
    9.42  val split_modifiers =
    9.43 - [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
    9.44 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
    9.45 -  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
    9.46 + [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
    9.47 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
    9.48 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
    9.49  
    9.50 -val split_args = #2 oo Method.syntax Attrib.local_thms;
    9.51 -
    9.52 -fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
    9.53 +fun split_meth src =
    9.54 +  Method.syntax Attrib.local_thms src
    9.55 +  #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
    9.56  
    9.57  
    9.58 -
    9.59 -(** theory setup **)
    9.60 +(* theory setup *)
    9.61  
    9.62  val setup =
    9.63 - [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
    9.64 -  Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
    9.65 + [Attrib.add_attributes
    9.66 +  [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
    9.67 +    "declaration of case split rule")],
    9.68 +  Method.add_methods [(splitN, split_meth, "apply case split rule")]];
    9.69  
    9.70  end;
    10.1 --- a/src/Pure/simplifier.ML	Sat Jan 14 17:20:51 2006 +0100
    10.2 +++ b/src/Pure/simplifier.ML	Sat Jan 14 22:25:34 2006 +0100
    10.3 @@ -64,16 +64,11 @@
    10.4    val print_local_simpset: Proof.context -> unit
    10.5    val get_local_simpset: Proof.context -> simpset
    10.6    val put_local_simpset: simpset -> Proof.context -> Proof.context
    10.7 -  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
    10.8 -  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
    10.9 -  val simp_add_global: theory attribute
   10.10 -  val simp_del_global: theory attribute
   10.11 -  val simp_add_local: Proof.context attribute
   10.12 -  val simp_del_local: Proof.context attribute
   10.13 -  val cong_add_global: theory attribute
   10.14 -  val cong_del_global: theory attribute
   10.15 -  val cong_add_local: Proof.context attribute
   10.16 -  val cong_del_local: Proof.context attribute
   10.17 +  val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
   10.18 +  val simp_add: Context.generic attribute
   10.19 +  val simp_del: Context.generic attribute
   10.20 +  val cong_add: Context.generic attribute
   10.21 +  val cong_del: Context.generic attribute
   10.22    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   10.23    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
   10.24    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   10.25 @@ -143,18 +138,14 @@
   10.26  
   10.27  (* attributes *)
   10.28  
   10.29 -fun change_global_ss f (thy, th) = (change_simpset_of thy (fn ss => f (ss, [th])); (thy, th));
   10.30 -fun change_local_ss f (ctxt, th) = (LocalSimpset.map (fn ss => f (ss, [th])) ctxt, th);
   10.31 +fun attrib f = Attrib.declaration (fn th =>
   10.32 +   fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
   10.33 +    | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
   10.34  
   10.35 -val simp_add_global = change_global_ss (op addsimps);
   10.36 -val simp_del_global = change_global_ss (op delsimps);
   10.37 -val simp_add_local = change_local_ss (op addsimps);
   10.38 -val simp_del_local = change_local_ss (op delsimps);
   10.39 -
   10.40 -val cong_add_global = change_global_ss (op addcongs);
   10.41 -val cong_del_global = change_global_ss (op delcongs);
   10.42 -val cong_add_local = change_local_ss (op addcongs);
   10.43 -val cong_del_local = change_local_ss (op delcongs);
   10.44 +val simp_add = attrib (op addsimps);
   10.45 +val simp_del = attrib (op delsimps);
   10.46 +val cong_add = attrib (op addcongs);
   10.47 +val cong_del = attrib (op delcongs);
   10.48  
   10.49  
   10.50  
   10.51 @@ -243,14 +234,6 @@
   10.52  val no_asm_simpN = "no_asm_simp";
   10.53  val asm_lrN = "asm_lr";
   10.54  
   10.55 -val simp_attr =
   10.56 - (Attrib.add_del_args simp_add_global simp_del_global,
   10.57 -  Attrib.add_del_args simp_add_local simp_del_local);
   10.58 -
   10.59 -val cong_attr =
   10.60 - (Attrib.add_del_args cong_add_global cong_del_global,
   10.61 -  Attrib.add_del_args cong_add_local cong_del_local);
   10.62 -
   10.63  
   10.64  (* conversions *)
   10.65  
   10.66 @@ -262,15 +245,14 @@
   10.67      Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   10.68      Scan.succeed asm_full_simplify) |> Scan.lift) x;
   10.69  
   10.70 -fun simplified_att get args =
   10.71 -  Attrib.syntax (conv_mode -- args >> (fn (f, ths) => Attrib.rule (fn x =>
   10.72 -    f ((if null ths then I else MetaSimplifier.clear_ss) (get x) addsimps ths))));
   10.73 +fun get_ss (Context.Theory thy) = simpset_of thy
   10.74 +  | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
   10.75  
   10.76  in
   10.77  
   10.78 -val simplified_attr =
   10.79 - (simplified_att simpset_of Attrib.global_thmss,
   10.80 -  simplified_att local_simpset_of Attrib.local_thmss);
   10.81 +val simplified =
   10.82 +  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
   10.83 +    f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
   10.84  
   10.85  end;
   10.86  
   10.87 @@ -279,9 +261,11 @@
   10.88  
   10.89  val _ = Context.add_setup
   10.90   [Attrib.add_attributes
   10.91 -   [(simpN, simp_attr, "declaration of simplification rule"),
   10.92 -    (congN, cong_attr, "declaration of Simplifier congruence rule"),
   10.93 -    ("simplified", simplified_attr, "simplified rule")]];
   10.94 +   [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   10.95 +      "declaration of Simplifier rule"),
   10.96 +    (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   10.97 +      "declaration of Simplifier congruence rule"),
   10.98 +    ("simplified", Attrib.common simplified, "simplified rule")]];
   10.99  
  10.100  
  10.101  
  10.102 @@ -302,22 +286,23 @@
  10.103    >> (curry (Library.foldl op o) I o rev)) x;
  10.104  
  10.105  val cong_modifiers =
  10.106 - [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local): Method.modifier),
  10.107 -  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
  10.108 -  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
  10.109 + [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
  10.110 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
  10.111 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
  10.112  
  10.113  val simp_modifiers =
  10.114 - [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
  10.115 -  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
  10.116 -  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
  10.117 + [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
  10.118 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
  10.119 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
  10.120    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
  10.121 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
  10.122 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
  10.123     @ cong_modifiers;
  10.124  
  10.125  val simp_modifiers' =
  10.126 - [Args.add -- Args.colon >> K (I, simp_add_local),
  10.127 -  Args.del -- Args.colon >> K (I, simp_del_local),
  10.128 -  Args.$$$ onlyN -- Args.colon >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
  10.129 + [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
  10.130 +  Args.del -- Args.colon >> K (I, Attrib.context simp_del),
  10.131 +  Args.$$$ onlyN -- Args.colon
  10.132 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
  10.133     @ cong_modifiers;
  10.134  
  10.135  fun simp_args more_mods =
    11.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
    11.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
    11.3 @@ -367,8 +367,8 @@
    11.4    (*Updating theory components: simprules and datatype info*)
    11.5    (thy1 |> Theory.add_path big_rec_base_name
    11.6          |> PureThy.add_thmss
    11.7 -         [(("simps", simps), [Simplifier.simp_add_global]),
    11.8 -          (("", intrs), [Classical.safe_intro_global]),
    11.9 +         [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
   11.10 +          (("", intrs), [Attrib.theory Classical.safe_intro]),
   11.11            (("con_defs", con_defs), []),
   11.12            (("case_eqns", case_eqns), []),
   11.13            (("recursor_eqns", recursor_eqns), []),
    12.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 17:20:51 2006 +0100
    12.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jan 14 22:25:34 2006 +0100
    12.3 @@ -165,7 +165,7 @@
    12.4    in
    12.5      thy
    12.6      |> Theory.add_path (Sign.base_name big_rec_name)
    12.7 -    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
    12.8 +    |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
    12.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   12.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   12.11      |> Theory.parent_path
    13.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
    13.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
    13.3 @@ -191,7 +191,7 @@
    13.4        |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
    13.5      val (_, thy3) =
    13.6        thy2
    13.7 -      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]
    13.8 +      |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])]
    13.9        ||> Theory.parent_path;
   13.10    in (thy3, eqn_thms') end;
   13.11