# HG changeset patch
# User wenzelm
# Date 1320612706 -3600
# Node ID 7fe19930dfc9136b136262884a8e7dc422083bff
# Parent  e99fd663c4a3c3bcdd91ca1a072827ab1c951684
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
misc tuning;

diff -r e99fd663c4a3 -r 7fe19930dfc9 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -633,6 +633,7 @@
 in
 val hol4_setup =
   initial_maps #>
-  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
+  Attrib.setup @{binding hol4rew}
+    (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule"
 
 end
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -536,8 +536,13 @@
 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
 val add_inductive = Inductive.gen_add_inductive add_ind_set_def;
 
-val mono_add_att = to_pred_att [] #> Inductive.mono_add;
-val mono_del_att = to_pred_att [] #> Inductive.mono_del;
+fun mono_att att =  (* FIXME really mixed_attribute!? *)
+  Thm.mixed_attribute (fn (context, thm) =>
+    let val thm' = to_pred [] context thm
+    in (Thm.attribute_declaration att thm' context, thm') end);
+
+val mono_add_att = mono_att Inductive.mono_add;
+val mono_del_att = mono_att Inductive.mono_del;
 
 
 (** package setup **)
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Provers/clasimp.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -66,8 +66,6 @@
   Also ~A goes to the Safe Elim rule A ==> ?R
   Failing other cases, A is added as a Safe Intr rule*)
 
-fun app (att: attribute) th context = #1 (att (context, th));
-
 fun add_iff safe unsafe =
   Thm.declaration_attribute (fn th =>
     let
@@ -75,25 +73,30 @@
       val (elim, intro) = if n = 0 then safe else unsafe;
       val zero_rotate = zero_var_indexes o rotate_prems n;
     in
-      app intro (zero_rotate (th RS Data.iffD2)) #>
-      app elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
-      handle THM _ => (app elim (zero_rotate (th RS Data.notE)) handle THM _ => app intro th)
+      Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
+      Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
+      handle THM _ =>
+        (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
+          handle THM _ => Thm.attribute_declaration intro th)
     end);
 
 fun del_iff del = Thm.declaration_attribute (fn th =>
   let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
-    app del (zero_rotate (th RS Data.iffD2)) #>
-    app del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
-    handle THM _ => (app del (zero_rotate (th RS Data.notE)) handle THM _ => app del th)
+    Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
+    Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
+    handle THM _ =>
+      (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
+        handle THM _ => Thm.attribute_declaration del th)
   end);
 
 in
 
 val iff_add =
-  add_iff
-    (Classical.safe_elim NONE, Classical.safe_intro NONE)
-    (Classical.haz_elim NONE, Classical.haz_intro NONE)
-  #> Simplifier.simp_add;
+  Thm.declaration_attribute (fn th =>
+    Thm.attribute_declaration (add_iff
+      (Classical.safe_elim NONE, Classical.safe_intro NONE)
+      (Classical.haz_elim NONE, Classical.haz_intro NONE)) th
+    #> Thm.attribute_declaration Simplifier.simp_add th);
 
 val iff_add' =
   add_iff
@@ -101,9 +104,10 @@
     (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
 
 val iff_del =
-  del_iff Classical.rule_del #>
-  del_iff Context_Rules.rule_del #>
-  Simplifier.simp_del;
+  Thm.declaration_attribute (fn th =>
+    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
+    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
+    Thm.attribute_declaration Simplifier.simp_del th);
 
 end;
 
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Provers/classical.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -848,7 +848,11 @@
 val haz_elim = attrib o addE;
 val haz_intro = attrib o addI;
 val haz_dest = attrib o addD;
-val rule_del = attrib delrule o Context_Rules.rule_del;
+
+val rule_del =
+  Thm.declaration_attribute (fn th => fn context =>
+    context |> map_cs (delrule (SOME context) th) |>
+    Thm.attribute_declaration Context_Rules.rule_del th);
 
 
 
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -149,8 +149,9 @@
   thm structure.*)
 
 fun crude_closure ctxt src =
- (try (fn () => attribute_i (Proof_Context.theory_of ctxt) src
-    (Context.Proof ctxt, Drule.asm_rl)) ();
+ (try (fn () =>
+    Thm.apply_attribute (attribute_i (Proof_Context.theory_of ctxt) src)
+      (Context.Proof ctxt, Drule.asm_rl)) ();
   Args.closure src);
 
 
@@ -198,7 +199,8 @@
     Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
       let
         val atts = map (attribute_i thy) srcs;
-        val (context', th') = Library.apply atts (context, Drule.dummy_thm);
+        val (context', th') =
+          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
       in (context', pick "" [th']) end)
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
@@ -210,7 +212,8 @@
       let
         val ths = Facts.select thmref fact;
         val atts = map (attribute_i thy) srcs;
-        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
+        val (context', ths') =
+          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
       in (context', pick name ths') end)
   end);
 
@@ -247,7 +250,9 @@
 
 (* rename_abs *)
 
-fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
+val rename_abs =
+  Scan.repeat (Args.maybe Args.name)
+  >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
 
 
 (* unfold / fold definitions *)
@@ -269,18 +274,12 @@
 
 (* case names *)
 
-fun hname NONE = Rule_Cases.case_hypsN
-  | hname (SOME n) = n;
-
-fun case_names cs =
-  Rule_Cases.case_names (map fst cs) #>
-  Rule_Cases.cases_hyp_names (map (map hname o snd) cs);
-
-val hnamesP =
-  Scan.optional
-    (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [];
-
-fun case_namesP x = Scan.lift (Scan.repeat1 (Args.name -- hnamesP)) x;
+val case_names =
+  Scan.repeat1 (Args.name --
+    Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
+  (fn cs =>
+    Rule_Cases.cases_hyp_names (map fst cs)
+      (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
 
 
 (* misc rules *)
@@ -316,8 +315,7 @@
     "number of consumed facts" #>
   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
     "number of equality constraints" #>
-  setup (Binding.name "case_names") (case_namesP >> case_names)
-    "named rule cases" #>
+  setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
   setup (Binding.name "case_conclusion")
     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
     "named conclusion of rule cases" #>
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -72,12 +72,14 @@
 val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
 
 val sym_add =
-  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
-  #> Context_Rules.elim_query NONE;
+  Thm.declaration_attribute (fn th =>
+    (Data.map o apfst o apsnd) (Thm.add_thm th) #>
+    Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
 
 val sym_del =
-  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
-  #> Context_Rules.rule_del;
+  Thm.declaration_attribute (fn th =>
+    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
+    Thm.attribute_declaration Context_Rules.rule_del th);
 
 
 (* symmetric *)
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -80,7 +80,7 @@
       (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
   end;
 
-fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
+fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
     fun del b netpair = Tactic.delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
@@ -89,6 +89,8 @@
     else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   end;
 
+fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
+
 structure Rules = Generic_Data
 (
   type T = rules;
@@ -179,11 +181,11 @@
 
 (* add and del rules *)
 
-fun rule_del (x, th) =
-  (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
+
+val rule_del = Thm.declaration_attribute (fn th => Rules.map (del_rule th));
 
 fun rule_add k view opt_w =
-  (fn (x, th) => (Rules.map (add_rule k opt_w (view th)) x, th)) o rule_del;
+  Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th));
 
 val intro_bang  = rule_add intro_bangK I;
 val elim_bang   = rule_add elim_bangK I;
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -396,7 +396,8 @@
 local
 
 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
-fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths);
+fun app (f, att) (context, ths) =
+  Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
 
 in
 
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -117,7 +117,7 @@
 
 fun locale_notes locale kind global_facts local_facts lthy =
   let
-    val global_facts' = Attrib.map_facts (K I) global_facts;
+    val global_facts' = Attrib.map_facts (K (Thm.mixed_attribute I)) global_facts;
     val local_facts' = Element.facts_map
       (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
   in
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -207,7 +207,7 @@
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;
 
-fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
-fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
+val rule_format = Thm.rule_attribute (K rulify);
+val rule_format_no_asm = Thm.rule_attribute (K rulify_no_asm);
 
 end;
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -33,15 +33,16 @@
   val apply: term list -> T -> T
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
+  val get_consumes: thm -> int
+  val put_consumes: int option -> thm -> thm
   val add_consumes: int -> thm -> thm
-  val get_consumes: thm -> int
+  val default_consumes: int -> thm -> thm
   val consumes: int -> attribute
-  val consumes_default: int -> attribute
   val get_constraints: thm -> int
   val constraints: int -> attribute
   val name: string list -> thm -> thm
   val case_names: string list -> attribute
-  val cases_hyp_names: string list list -> attribute
+  val cases_hyp_names: string list -> string list list -> attribute
   val case_conclusion: string * string list -> attribute
   val is_inner_rule: thm -> bool
   val inner_rule: attribute
@@ -241,13 +242,13 @@
 
 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
 
+fun default_consumes n th =
+  if is_some (lookup_consumes th) then th else put_consumes (SOME n) th;
+
 val save_consumes = put_consumes o lookup_consumes;
 
 fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
 
-fun consumes_default n x =
-  if is_some (lookup_consumes (#2 x)) then x else consumes n x;
-
 
 
 (** equality constraints **)
@@ -292,7 +293,8 @@
 
 val save_case_names = add_case_names o lookup_case_names;
 val name = add_case_names o SOME;
-fun case_names ss = Thm.rule_attribute (K (name ss));
+fun case_names cs = Thm.rule_attribute (K (name cs));
+
 
 
 (** hyp names **)
@@ -312,8 +314,9 @@
   |> Option.map explode_hyps;
 
 val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
-fun cases_hyp_names ss =
-  Thm.rule_attribute (K (add_cases_hyp_names (SOME ss)));
+fun cases_hyp_names cs hs =
+  Thm.rule_attribute (K (name cs #> add_cases_hyp_names (SOME hs)));
+
 
 
 (** case conclusions **)
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/more_thm.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -12,7 +12,7 @@
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
-  type attribute = Context.generic * thm -> Context.generic * thm
+  type attribute = Context.generic * thm -> Context.generic option * thm option
 end;
 
 signature THM =
@@ -67,11 +67,14 @@
   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
-  type attribute = Context.generic * thm -> Context.generic * thm
+  type attribute = Context.generic * thm -> Context.generic option * thm option
   type binding = binding * attribute list
   val empty_binding: binding
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
+  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
+  val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm
+  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
   val theory_attributes: attribute list -> theory * thm -> theory * thm
   val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
   val no_attributes: 'a -> 'a * 'b list
@@ -391,18 +394,25 @@
 (** attributes **)
 
 (*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic * thm;
+type attribute = Context.generic * thm -> Context.generic option * thm option;
 
 type binding = binding * attribute list;
 val empty_binding: binding = (Binding.empty, []);
 
-fun rule_attribute f (x, th) = (x, f x th);
-fun declaration_attribute f (x, th) = (f th x, th);
+fun rule_attribute f (x, th) = (NONE, SOME (f x th));
+fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
+fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
+
+fun apply_attribute att (x, th) =
+  let val (x', th') = att (x, th)
+  in (the_default x x', the_default th th') end;
+
+fun attribute_declaration att th x = #1 (apply_attribute att (x, th));
 
 fun apply_attributes mk dest =
   let
     fun app [] = I
-      | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs;
+      | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts;
   in app end;
 
 val theory_attributes = apply_attributes Context.Theory Context.the_theory;
@@ -420,8 +430,8 @@
 fun tag_rule tg = Thm.map_tags (insert (op =) tg);
 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
 
-fun tag tg x = rule_attribute (K (tag_rule tg)) x;
-fun untag s x = rule_attribute (K (untag_rule s)) x;
+fun tag tg = rule_attribute (K (tag_rule tg));
+fun untag s = rule_attribute (K (untag_rule s));
 
 
 (* def_name *)
@@ -456,7 +466,7 @@
 fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
 
 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
-fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
+fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
 
 
 open Thm;
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/simplifier.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -303,7 +303,8 @@
 val simproc_att =
   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
     Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
-  >> (Library.apply o map Morphism.form);
+  >> (fn atts => Thm.declaration_attribute (fn th =>
+        Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)));
 
 end;
 
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Tools/case_product.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Tools/case_product.ML
     Author:     Lars Noschinski, TU Muenchen
 
-Combines two case rules into a single one.
+Combine two case rules into a single one.
 
 Assumes that the theorems are of the form
   "[| C1; ...; Cm; A1 ==> P; ...; An ==> P |] ==> P"
@@ -13,12 +13,12 @@
   val combine: Proof.context -> thm -> thm -> thm
   val combine_annotated: Proof.context -> thm -> thm -> thm
   val setup: theory -> theory
-end;
+end
 
 structure Case_Product: CASE_PRODUCT =
 struct
 
-(*Instantiates the conclusion of thm2 to the one of thm1.*)
+(*instantiate the conclusion of thm2 to the one of thm1*)
 fun inst_concl thm1 thm2 =
   let
     val cconcl_of = Drule.strip_imp_concl o Thm.cprop_of
@@ -32,7 +32,7 @@
   in ((i_thm1, i_thm2), ctxt'') end
 
 (*
-Returns list of prems, where loose bounds have been replaced by frees.
+Return list of prems, where loose bounds have been replaced by frees.
 FIXME: Focus
 *)
 fun free_prems t ctxt =
@@ -58,8 +58,7 @@
       in
         Logic.list_implies (t1 @ t2, concl)
         |> fold_rev Logic.all (subst1 @ subst2)
-      end
-      ) p_cases2) p_cases1
+      end) p_cases2) p_cases1
 
     val prems = p_cons1 :: p_cons2 :: p_cases_prod
   in
@@ -71,11 +70,10 @@
     val (p_cons1 :: p_cons2 :: premss) = unflat struc prems
     val thm2' = thm2 OF p_cons2
   in
-    (Tactic.rtac (thm1 OF p_cons1)
+    Tactic.rtac (thm1 OF p_cons1)
      THEN' EVERY' (map (fn p =>
        Tactic.rtac thm2'
        THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss)
-    )
   end
 
 fun combine ctxt thm1 thm2 =
@@ -86,22 +84,25 @@
     Goal.prove ctxt' [] (flat prems_rich) concl (fn {prems, ...} =>
       case_product_tac prems prems_rich i_thm1 i_thm2 1)
     |> singleton (Variable.export ctxt' ctxt)
-  end;
+  end
 
-fun annotation thm1 thm2 =
+fun annotation_rule thm1 thm2 =
   let
     val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
     val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
-    val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
+    val names = map_product (fn (x, _) => fn (y, _) => x ^ "_" ^ y) cases1 cases2
   in
-    Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
+    Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
   end
 
+fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
+
 fun combine_annotated ctxt thm1 thm2 =
   combine ctxt thm1 thm2
-  |> snd o annotation thm1 thm2 o pair (Context.Proof ctxt)
+  |> annotation_rule thm1 thm2
 
-(* Attribute setup *)
+
+(* attribute setup *)
 
 val case_prod_attr =
   let
@@ -112,6 +113,6 @@
   end
 
 val setup =
- Attrib.setup @{binding "case_product"} case_prod_attr "product with other case rules"
+  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
 
-end;
+end
diff -r e99fd663c4a3 -r 7fe19930dfc9 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Tools/induct.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -290,8 +290,12 @@
 
 local
 
-fun mk_att f g name arg =
-  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
+fun mk_att f g name =
+  Thm.mixed_attribute (fn (context, thm) =>
+    let
+      val thm' = g thm;
+      val context' = Data.map (f (name, thm')) context;
+    in (context', thm') end);
 
 fun del_att which =
   Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
@@ -309,8 +313,8 @@
 fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
 fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
 
-val consumes0 = Rule_Cases.consumes_default 0;
-val consumes1 = Rule_Cases.consumes_default 1;
+val consumes0 = Rule_Cases.default_consumes 0;
+val consumes1 = Rule_Cases.default_consumes 1;
 
 in