1.1 --- a/src/HOL/Import/hol4rews.ML	Sun Nov 06 21:17:45 2011 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Nov 06 21:51:46 2011 +0100
     1.3 @@ -633,6 +633,7 @@
     1.4  in
     1.5  val hol4_setup =
     1.6    initial_maps #>
     1.7 -  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
     1.8 +  Attrib.setup @{binding hol4rew}
     1.9 +    (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule"
    1.10  
    1.11  end

     2.1 --- a/src/HOL/Tools/inductive_set.ML	Sun Nov 06 21:17:45 2011 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 06 21:51:46 2011 +0100
     2.3 @@ -536,8 +536,13 @@
     2.4  val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
     2.5  val add_inductive = Inductive.gen_add_inductive add_ind_set_def;
     2.6  
     2.7 -val mono_add_att = to_pred_att [] #> Inductive.mono_add;
     2.8 -val mono_del_att = to_pred_att [] #> Inductive.mono_del;
     2.9 +fun mono_att att =  (* FIXME really mixed_attribute!? *)
    2.10 +  Thm.mixed_attribute (fn (context, thm) =>
    2.11 +    let val thm' = to_pred [] context thm
    2.12 +    in (Thm.attribute_declaration att thm' context, thm') end);
    2.13 +
    2.14 +val mono_add_att = mono_att Inductive.mono_add;
    2.15 +val mono_del_att = mono_att Inductive.mono_del;
    2.16  
    2.17  
    2.18  (** package setup **)

     3.1 --- a/src/Provers/clasimp.ML	Sun Nov 06 21:17:45 2011 +0100
     3.2 +++ b/src/Provers/clasimp.ML	Sun Nov 06 21:51:46 2011 +0100
     3.3 @@ -66,8 +66,6 @@
     3.4    Also ~A goes to the Safe Elim rule A ==> ?R
     3.5    Failing other cases, A is added as a Safe Intr rule*)
     3.6  
     3.7 -fun app (att: attribute) th context = #1 (att (context, th));
     3.8 -
     3.9  fun add_iff safe unsafe =
    3.10    Thm.declaration_attribute (fn th =>
    3.11      let
    3.12 @@ -75,25 +73,30 @@
    3.13        val (elim, intro) = if n = 0 then safe else unsafe;
    3.14        val zero_rotate = zero_var_indexes o rotate_prems n;
    3.15      in
    3.16 -      app intro (zero_rotate (th RS Data.iffD2)) #>
    3.17 -      app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
    3.18 -      handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th)
    3.19 +      Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
    3.20 +      Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
    3.21 +      handle THM _ =>
    3.22 +        (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
    3.23 +          handle THM _ => Thm.attribute_declaration intro th)
    3.24      end);
    3.25  
    3.26  fun del_iff del = Thm.declaration_attribute (fn th =>
    3.27    let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    3.28 -    app del (zero_rotate (th RS Data.iffD2)) #>
    3.29 -    app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
    3.30 -    handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th)
    3.31 +    Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
    3.32 +    Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
    3.33 +    handle THM _ =>
    3.34 +      (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
    3.35 +        handle THM _ => Thm.attribute_declaration del th)
    3.36    end);
    3.37  
    3.38  in
    3.39  
    3.40  val iff_add =
    3.41 -  add_iff
    3.42 -    (Classical.safe_elim NONE, Classical.safe_intro NONE)
    3.43 -    (Classical.haz_elim NONE, Classical.haz_intro NONE)
    3.44 -  #> Simplifier.simp_add;
    3.45 +  Thm.declaration_attribute (fn th =>
    3.46 +    Thm.attribute_declaration (add_iff
    3.47 +      (Classical.safe_elim NONE, Classical.safe_intro NONE)
    3.48 +      (Classical.haz_elim NONE, Classical.haz_intro NONE)) th
    3.49 +    #> Thm.attribute_declaration Simplifier.simp_add th);
    3.50  
    3.51  val iff_add' =
    3.52    add_iff
    3.53 @@ -101,9 +104,10 @@
    3.54      (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
    3.55  
    3.56  val iff_del =
    3.57 -  del_iff Classical.rule_del #>
    3.58 -  del_iff Context_Rules.rule_del #>
    3.59 -  Simplifier.simp_del;
    3.60 +  Thm.declaration_attribute (fn th =>
    3.61 +    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
    3.62 +    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
    3.63 +    Thm.attribute_declaration Simplifier.simp_del th);
    3.64  
    3.65  end;
    3.66  

     4.1 --- a/src/Provers/classical.ML	Sun Nov 06 21:17:45 2011 +0100
     4.2 +++ b/src/Provers/classical.ML	Sun Nov 06 21:51:46 2011 +0100
     4.3 @@ -848,7 +848,11 @@
     4.4  val haz_elim = attrib o addE;
     4.5  val haz_intro = attrib o addI;
     4.6  val haz_dest = attrib o addD;
     4.7 -val rule_del = attrib delrule o Context_Rules.rule_del;
     4.8 +
     4.9 +val rule_del =
    4.10 +  Thm.declaration_attribute (fn th => fn context =>
    4.11 +    context |> map_cs (delrule (SOME context) th) |>
    4.12 +    Thm.attribute_declaration Context_Rules.rule_del th);
    4.13  
    4.14  
    4.15  

     5.1 --- a/src/Pure/Isar/attrib.ML	Sun Nov 06 21:17:45 2011 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 06 21:51:46 2011 +0100
     5.3 @@ -149,8 +149,9 @@
     5.4    thm structure.*)
     5.5  
     5.6  fun crude_closure ctxt src =
     5.7 - (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
     5.8 -    (Context.Proof ctxt, Drule.asm_rl)) ();
     5.9 + (try (fn () =>
    5.10 +    Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
    5.11 +      (Context.Proof ctxt, Drule.asm_rl)) ();
    5.12    Args.closure src);
    5.13  
    5.14  
    5.15 @@ -198,7 +199,8 @@
    5.16      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    5.17        let
    5.18          val atts = map (attribute_i thy) srcs;
    5.19 -        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    5.20 +        val (context', th') =
    5.21 +          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
    5.22        in (context', pick "" [th']) end)
    5.23      ||
    5.24      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    5.25 @@ -210,7 +212,8 @@
    5.26        let
    5.27          val ths = Facts.select thmref fact;
    5.28          val atts = map (attribute_i thy) srcs;
    5.29 -        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
    5.30 +        val (context', ths') =
    5.31 +          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
    5.32        in (context', pick name ths') end)
    5.33    end);
    5.34  
    5.35 @@ -247,7 +250,9 @@
    5.36  
    5.37  (* rename_abs *)
    5.38  
    5.39 -fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
    5.40 +val rename_abs =
    5.41 +  Scan.repeat (Args.maybe Args.name)
    5.42 +  >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
    5.43  
    5.44  
    5.45  (* unfold / fold definitions *)
    5.46 @@ -269,18 +274,12 @@
    5.47  
    5.48  (* case names *)
    5.49  
    5.50 -fun hname NONE = Rule_Cases.case_hypsN
    5.51 -  | hname (SOME n) = n;
    5.52 -
    5.53 -fun case_names cs =
    5.54 -  Rule_Cases.case_names (map fst cs) #>
    5.55 -  Rule_Cases.cases_hyp_names (map (map hname o snd) cs);
    5.56 -
    5.57 -val hnamesP =
    5.58 -  Scan.optional
    5.59 -    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [];
    5.60 -
    5.61 -fun case_namesP x = Scan.lift (Scan.repeat1 (Args.name -- hnamesP)) x;
    5.62 +val case_names =
    5.63 +  Scan.repeat1 (Args.name --
    5.64 +    Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
    5.65 +  (fn cs =>
    5.66 +    Rule_Cases.cases_hyp_names (map fst cs)
    5.67 +      (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
    5.68  
    5.69  
    5.70  (* misc rules *)
    5.71 @@ -316,8 +315,7 @@
    5.72      "number of consumed facts" #>
    5.73    setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    5.74      "number of equality constraints" #>
    5.75 -  setup (Binding.name "case_names") (case_namesP >> case_names)
    5.76 -    "named rule cases" #>
    5.77 +  setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
    5.78    setup (Binding.name "case_conclusion")
    5.79      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    5.80      "named conclusion of rule cases" #>

     6.1 --- a/src/Pure/Isar/calculation.ML	Sun Nov 06 21:17:45 2011 +0100
     6.2 +++ b/src/Pure/Isar/calculation.ML	Sun Nov 06 21:51:46 2011 +0100
     6.3 @@ -72,12 +72,14 @@
     6.4  val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
     6.5  
     6.6  val sym_add =
     6.7 -  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
     6.8 -  #> Context_Rules.elim_query NONE;
     6.9 +  Thm.declaration_attribute (fn th =>
    6.10 +    (Data.map o apfst o apsnd) (Thm.add_thm th) #>
    6.11 +    Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
    6.12  
    6.13  val sym_del =
    6.14 -  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
    6.15 -  #> Context_Rules.rule_del;
    6.16 +  Thm.declaration_attribute (fn th =>
    6.17 +    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
    6.18 +    Thm.attribute_declaration Context_Rules.rule_del th);
    6.19  
    6.20  
    6.21  (* symmetric *)

     7.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:17:45 2011 +0100
     7.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:51:46 2011 +0100
     7.3 @@ -80,7 +80,7 @@
     7.4        (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     7.5    end;
     7.6  
     7.7 -fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
     7.8 +fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
     7.9    let
    7.10      fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
    7.11      fun del b netpair = Tactic.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
    7.12 @@ -89,6 +89,8 @@
    7.13      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
    7.14    end;
    7.15  
    7.16 +fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
    7.17 +
    7.18  structure Rules = Generic_Data
    7.19  (
    7.20    type T = rules;
    7.21 @@ -179,11 +181,11 @@
    7.22  
    7.23  (* add and del rules *)
    7.24  
    7.25 -fun rule_del (x, th) =
    7.26 -  (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
    7.27 +
    7.28 +val rule_del = Thm.declaration_attribute (fn th => Rules.map (del_rule th));
    7.29  
    7.30  fun rule_add k view opt_w =
    7.31 -  (fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del;
    7.32 +  Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th));
    7.33  
    7.34  val intro_bang  = rule_add intro_bangK I;
    7.35  val elim_bang   = rule_add elim_bangK I;

     8.1 --- a/src/Pure/Isar/method.ML	Sun Nov 06 21:17:45 2011 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 06 21:51:46 2011 +0100
     8.3 @@ -396,7 +396,8 @@
     8.4  local
     8.5  
     8.6  fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
     8.7 -fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths);
     8.8 +fun app (f, att) (context, ths) =
     8.9 +  Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
    8.10  
    8.11  in
    8.12  

     9.1 --- a/src/Pure/Isar/named_target.ML	Sun Nov 06 21:17:45 2011 +0100
     9.2 +++ b/src/Pure/Isar/named_target.ML	Sun Nov 06 21:51:46 2011 +0100
     9.3 @@ -117,7 +117,7 @@
     9.4  
     9.5  fun locale_notes locale kind global_facts local_facts lthy =
     9.6    let
     9.7 -    val global_facts' = Attrib.map_facts (K I) global_facts;
     9.8 +    val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
     9.9      val local_facts' = Element.facts_map
    9.10        (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
    9.11    in

    10.1 --- a/src/Pure/Isar/object_logic.ML	Sun Nov 06 21:17:45 2011 +0100
    10.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Nov 06 21:51:46 2011 +0100
    10.3 @@ -207,7 +207,7 @@
    10.4  val rulify = gen_rulify true;
    10.5  val rulify_no_asm = gen_rulify false;
    10.6  
    10.7 -fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
    10.8 -fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
    10.9 +val rule_format = Thm.rule_attribute (K rulify);
   10.10 +val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
   10.11  
   10.12  end;

    11.1 --- a/src/Pure/Isar/rule_cases.ML	Sun Nov 06 21:17:45 2011 +0100
    11.2 +++ b/src/Pure/Isar/rule_cases.ML	Sun Nov 06 21:51:46 2011 +0100
    11.3 @@ -33,15 +33,16 @@
    11.4    val apply: term list -> T -> T
    11.5    val consume: thm list -> thm list -> ('a * int) * thm ->
    11.6      (('a * (int * thm list)) * thm) Seq.seq
    11.7 +  val get_consumes: thm -> int
    11.8 +  val put_consumes: int option -> thm -> thm
    11.9    val add_consumes: int -> thm -> thm
   11.10 -  val get_consumes: thm -> int
   11.11 +  val default_consumes: int -> thm -> thm
   11.12    val consumes: int -> attribute
   11.13 -  val consumes_default: int -> attribute
   11.14    val get_constraints: thm -> int
   11.15    val constraints: int -> attribute
   11.16    val name: string list -> thm -> thm
   11.17    val case_names: string list -> attribute
   11.18 -  val cases_hyp_names: string list list -> attribute
   11.19 +  val cases_hyp_names: string list -> string list list -> attribute
   11.20    val case_conclusion: string * string list -> attribute
   11.21    val is_inner_rule: thm -> bool
   11.22    val inner_rule: attribute
   11.23 @@ -241,13 +242,13 @@
   11.24  
   11.25  fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   11.26  
   11.27 +fun default_consumes n th =
   11.28 +  if is_some (lookup_consumes th) then th else put_consumes (SOME n) th;
   11.29 +
   11.30  val save_consumes = put_consumes o lookup_consumes;
   11.31  
   11.32  fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
   11.33  
   11.34 -fun consumes_default n x =
   11.35 -  if is_some (lookup_consumes (#2 x)) then x else consumes n x;
   11.36 -
   11.37  
   11.38  
   11.39  (** equality constraints **)
   11.40 @@ -292,7 +293,8 @@
   11.41  
   11.42  val save_case_names = add_case_names o lookup_case_names;
   11.43  val name = add_case_names o SOME;
   11.44 -fun case_names ss = Thm.rule_attribute (K (name ss));
   11.45 +fun case_names cs = Thm.rule_attribute (K (name cs));
   11.46 +
   11.47  
   11.48  
   11.49  (** hyp names **)
   11.50 @@ -312,8 +314,9 @@
   11.51    |> Option.map explode_hyps;
   11.52  
   11.53  val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
   11.54 -fun cases_hyp_names ss =
   11.55 -  Thm.rule_attribute (K (add_cases_hyp_names (SOME ss)));
   11.56 +fun cases_hyp_names cs hs =
   11.57 +  Thm.rule_attribute (K (name cs #> add_cases_hyp_names (SOME hs)));
   11.58 +
   11.59  
   11.60  
   11.61  (** case conclusions **)

    12.1 --- a/src/Pure/more_thm.ML	Sun Nov 06 21:17:45 2011 +0100
    12.2 +++ b/src/Pure/more_thm.ML	Sun Nov 06 21:51:46 2011 +0100
    12.3 @@ -12,7 +12,7 @@
    12.4    structure Ctermtab: TABLE
    12.5    structure Thmtab: TABLE
    12.6    val aconvc: cterm * cterm -> bool
    12.7 -  type attribute = Context.generic * thm -> Context.generic * thm
    12.8 +  type attribute = Context.generic * thm -> Context.generic option * thm option
    12.9  end;
   12.10  
   12.11  signature THM =
   12.12 @@ -67,11 +67,14 @@
   12.13    val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   12.14    val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   12.15    val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   12.16 -  type attribute = Context.generic * thm -> Context.generic * thm
   12.17 +  type attribute = Context.generic * thm -> Context.generic option * thm option
   12.18    type binding = binding * attribute list
   12.19    val empty_binding: binding
   12.20    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   12.21    val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   12.22 +  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
   12.23 +  val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm
   12.24 +  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
   12.25    val theory_attributes: attribute list -> theory * thm -> theory * thm
   12.26    val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
   12.27    val no_attributes: 'a -> 'a * 'b list
   12.28 @@ -391,18 +394,25 @@
   12.29  (** attributes **)
   12.30  
   12.31  (*attributes subsume any kind of rules or context modifiers*)
   12.32 -type attribute = Context.generic * thm -> Context.generic * thm;
   12.33 +type attribute = Context.generic * thm -> Context.generic option * thm option;
   12.34  
   12.35  type binding = binding * attribute list;
   12.36  val empty_binding: binding = (Binding.empty, []);
   12.37  
   12.38 -fun rule_attribute f (x, th) = (x, f x th);
   12.39 -fun declaration_attribute f (x, th) = (f th x, th);
   12.40 +fun rule_attribute f (x, th) = (NONE, SOME (f x th));
   12.41 +fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
   12.42 +fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
   12.43 +
   12.44 +fun apply_attribute att (x, th) =
   12.45 +  let val (x', th') = att (x, th)
   12.46 +  in (the_default x x', the_default th th') end;
   12.47 +
   12.48 +fun attribute_declaration att th x = #1 (apply_attribute att (x, th));
   12.49  
   12.50  fun apply_attributes mk dest =
   12.51    let
   12.52      fun app [] = I
   12.53 -      | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs;
   12.54 +      | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts;
   12.55    in app end;
   12.56  
   12.57  val theory_attributes = apply_attributes Context.Theory Context.the_theory;
   12.58 @@ -420,8 +430,8 @@
   12.59  fun tag_rule tg = Thm.map_tags (insert (op =) tg);
   12.60  fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
   12.61  
   12.62 -fun tag tg x = rule_attribute (K (tag_rule tg)) x;
   12.63 -fun untag s x = rule_attribute (K (untag_rule s)) x;
   12.64 +fun tag tg = rule_attribute (K (tag_rule tg));
   12.65 +fun untag s = rule_attribute (K (untag_rule s));
   12.66  
   12.67  
   12.68  (* def_name *)
   12.69 @@ -456,7 +466,7 @@
   12.70  fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
   12.71  
   12.72  fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
   12.73 -fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
   12.74 +fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
   12.75  
   12.76  
   12.77  open Thm;

    13.1 --- a/src/Pure/simplifier.ML	Sun Nov 06 21:17:45 2011 +0100
    13.2 +++ b/src/Pure/simplifier.ML	Sun Nov 06 21:51:46 2011 +0100
    13.3 @@ -303,7 +303,8 @@
    13.4  val simproc_att =
    13.5    (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
    13.6      Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
    13.7 -  >> (Library.apply o map Morphism.form);
    13.8 +  >> (fn atts => Thm.declaration_attribute (fn th =>
    13.9 +        Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)));
   13.10  
   13.11  end;
   13.12  

    14.1 --- a/src/Tools/case_product.ML	Sun Nov 06 21:17:45 2011 +0100
    14.2 +++ b/src/Tools/case_product.ML	Sun Nov 06 21:51:46 2011 +0100
    14.3 @@ -1,7 +1,7 @@
    14.4  (*  Title:      Tools/case_product.ML
    14.5      Author:     Lars Noschinski, TU Muenchen
    14.6  
    14.7 -Combines two case rules into a single one.
    14.8 +Combine two case rules into a single one.
    14.9  
   14.10  Assumes that the theorems are of the form
   14.11    "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
   14.12 @@ -13,12 +13,12 @@
   14.13    val combine: Proof.context -> thm -> thm -> thm
   14.14    val combine_annotated: Proof.context -> thm -> thm -> thm
   14.15    val setup: theory -> theory
   14.16 -end;
   14.17 +end
   14.18  
   14.19  structure Case_Product: CASE_PRODUCT =
   14.20  struct
   14.21  
   14.22 -(*Instantiates the conclusion of thm2 to the one of thm1.*)
   14.23 +(*instantiate the conclusion of thm2 to the one of thm1*)
   14.24  fun inst_concl thm1 thm2 =
   14.25    let
   14.26      val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
   14.27 @@ -32,7 +32,7 @@
   14.28    in ((i_thm1, i_thm2), ctxt'') end
   14.29  
   14.30  (*
   14.31 -Returns list of prems, where loose bounds have been replaced by frees.
   14.32 +Return list of prems, where loose bounds have been replaced by frees.
   14.33  FIXME: Focus
   14.34  *)
   14.35  fun free_prems t ctxt =
   14.36 @@ -58,8 +58,7 @@
   14.37        in
   14.38          Logic.list_implies (t1 @ t2, concl)
   14.39          |> fold_rev Logic.all (subst1 @ subst2)
   14.40 -      end
   14.41 -      ) p_cases2) p_cases1
   14.42 +      end) p_cases2) p_cases1
   14.43  
   14.44      val prems = p_cons1 :: p_cons2 :: p_cases_prod
   14.45    in
   14.46 @@ -71,11 +70,10 @@
   14.47      val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
   14.48      val thm2' = thm2 OF p_cons2
   14.49    in
   14.50 -    (Tactic.rtac (thm1 OF p_cons1)
   14.51 +    Tactic.rtac (thm1 OF p_cons1)
   14.52       THEN' EVERY' (map (fn p =>
   14.53         Tactic.rtac thm2'
   14.54         THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
   14.55 -    )
   14.56    end
   14.57  
   14.58  fun combine ctxt thm1 thm2 =
   14.59 @@ -86,22 +84,25 @@
   14.60      Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
   14.61        case_product_tac prems prems_rich i_thm1 i_thm2 1)
   14.62      |> singleton (Variable.export ctxt' ctxt)
   14.63 -  end;
   14.64 +  end
   14.65  
   14.66 -fun annotation thm1 thm2 =
   14.67 +fun annotation_rule thm1 thm2 =
   14.68    let
   14.69      val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
   14.70      val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
   14.71 -    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
   14.72 +    val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
   14.73    in
   14.74 -    Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
   14.75 +    Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
   14.76    end
   14.77  
   14.78 +fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
   14.79 +
   14.80  fun combine_annotated ctxt thm1 thm2 =
   14.81    combine ctxt thm1 thm2
   14.82 -  |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
   14.83 +  |> annotation_rule thm1 thm2
   14.84  
   14.85 -(* Attribute setup *)
   14.86 +
   14.87 +(* attribute setup *)
   14.88  
   14.89  val case_prod_attr =
   14.90    let
   14.91 @@ -112,6 +113,6 @@
   14.92    end
   14.93  
   14.94  val setup =
   14.95 - Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
   14.96 +  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
   14.97  
   14.98 -end;
   14.99 +end

    15.1 --- a/src/Tools/induct.ML	Sun Nov 06 21:17:45 2011 +0100
    15.2 +++ b/src/Tools/induct.ML	Sun Nov 06 21:51:46 2011 +0100
    15.3 @@ -290,8 +290,12 @@
    15.4  
    15.5  local
    15.6  
    15.7 -fun mk_att f g name arg =
    15.8 -  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
    15.9 +fun mk_att f g name =
   15.10 +  Thm.mixed_attribute (fn (context, thm) =>
   15.11 +    let
   15.12 +      val thm' = g thm;
   15.13 +      val context' = Data.map (f (name, thm')) context;
   15.14 +    in (context', thm') end);
   15.15  
   15.16  fun del_att which =
   15.17    Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
   15.18 @@ -309,8 +313,8 @@
   15.19  fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
   15.20  fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
   15.21  
   15.22 -val consumes0 = Rule_Cases.consumes_default 0;
   15.23 -val consumes1 = Rule_Cases.consumes_default 1;
   15.24 +val consumes0 = Rule_Cases.default_consumes 0;
   15.25 +val consumes1 = Rule_Cases.default_consumes 1;
   15.26  
   15.27  in
   15.28