# HG changeset patch
# User wenzelm
# Date 1136918016 -3600
# Node ID 33a6f6caa6172beb78d062bf3e5c3c94b792e2a0
# Parent  cb068cfdcac88637094d9441e47bfec3033dd2f7
generic data and attributes;
tuned;

diff -r cb068cfdcac8 -r 33a6f6caa617 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/calculation.ML	Tue Jan 10 19:33:36 2006 +0100
@@ -7,23 +7,16 @@
 
 signature CALCULATION =
 sig
+  val print_rules: Context.generic -> unit
   val get_calculation: Proof.state -> thm list option
-  val print_global_rules: theory -> unit
-  val print_local_rules: Proof.context -> unit
-  val trans_add_global: theory attribute
-  val trans_del_global: theory attribute
-  val trans_add_local: Proof.context attribute
-  val trans_del_local: Proof.context attribute
-  val sym_add_global: theory attribute
-  val sym_del_global: theory attribute
-  val sym_add_local: Proof.context attribute
-  val sym_del_local: Proof.context attribute
-  val symmetric_global: theory attribute
-  val symmetric_local: Proof.context attribute
+  val trans_add: Context.generic attribute
+  val trans_del: Context.generic attribute
+  val sym_add: Context.generic attribute
+  val sym_del: Context.generic attribute
+  val symmetric: Context.generic attribute
   val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val finally: (thmref * Attrib.src list) list option -> bool ->
-    Proof.state -> Proof.state Seq.seq
+  val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state
@@ -32,112 +25,85 @@
 structure Calculation: CALCULATION =
 struct
 
-(** global and local calculation data **)
-
-(* global calculation *)
-
-fun print_rules prt x (trans, sym) =
-  [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)),
-    Pretty.big_list "symmetry rules:" (map (prt x) sym)]
-  |> Pretty.chunks |> Pretty.writeln;
-
-structure GlobalCalculation = TheoryDataFun
-(struct
-  val name = "Isar/calculation";
-  type T = thm NetRules.T * thm list
+(** calculation data **)
 
-  val empty = (NetRules.elim, []);
-  val copy = I;
-  val extend = I;
-  fun merge _ ((trans1, sym1), (trans2, sym2)) =
-    (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2));
-  val print = print_rules Display.pretty_thm_sg;
-end);
-
-val _ = Context.add_setup [GlobalCalculation.init];
-val print_global_rules = GlobalCalculation.print;
-
-
-(* local calculation *)
-
-structure LocalCalculation = ProofDataFun
-(struct
+structure CalculationData = GenericDataFun
+(
   val name = "Isar/calculation";
   type T = (thm NetRules.T * thm list) * (thm list * int) option;
+  val empty = ((NetRules.elim, []), NONE);
+  val extend = I;
 
-  fun init thy = (GlobalCalculation.get thy, NONE);
-  fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
-end);
+  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
+    ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
 
-val _ = Context.add_setup [LocalCalculation.init];
-val get_local_rules = #1 o LocalCalculation.get o Proof.context_of;
-val print_local_rules = LocalCalculation.print;
+  fun print generic ((trans, sym), _) =
+    let val ctxt = Context.proof_of generic in
+      [Pretty.big_list "transitivity rules:"
+          (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
+        Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+      |> Pretty.chunks |> Pretty.writeln
+    end;
+);
+
+val _ = Context.add_setup [CalculationData.init];
+val print_rules = CalculationData.print;
 
 
 (* access calculation *)
 
 fun get_calculation state =
-  (case #2 (LocalCalculation.get (Proof.context_of state)) of
+  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
     NONE => NONE
   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
 
 val calculationN = "calculation";
 
 fun put_calculation calc =
-  `Proof.level #-> (fn lev => Proof.map_context
-    (LocalCalculation.map (apsnd (K (Option.map (rpair lev) calc)))))
+  `Proof.level #-> (fn lev =>
+    Proof.map_context (Context.the_proof o
+        CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
   #> Proof.put_thms (calculationN, calc);
 
 
+
 (** attributes **)
 
 (* add/del rules *)
 
-fun global_att f (x, thm) = (GlobalCalculation.map (f thm) x, thm);
-fun local_att f (x, thm) = (LocalCalculation.map (apfst (f thm)) x, thm);
+val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
+val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
 
-val trans_add_global = global_att (apfst o NetRules.insert);
-val trans_del_global = global_att (apfst o NetRules.delete);
-val trans_add_local = local_att (apfst o NetRules.insert);
-val trans_del_local = local_att (apfst o NetRules.delete);
-
-val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
-val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
-val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
-val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
+val sym_add =
+  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
+  #> ContextRules.elim_query NONE;
+val sym_del =
+  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
+  #> ContextRules.rule_del;
 
 
-(* symmetry *)
+(* symmetric *)
 
-fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
-  (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
+val symmetric = Attrib.rule (fn x => fn th =>
+  (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
     ([th'], _) => th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
 
-val symmetric_global = gen_symmetric (#2 o GlobalCalculation.get);
-val symmetric_local = gen_symmetric (#2 o #1 o LocalCalculation.get);
-
 
 (* concrete syntax *)
 
-val trans_attr =
- (Attrib.add_del_args trans_add_global trans_del_global,
-  Attrib.add_del_args trans_add_local trans_del_local);
-
-val sym_attr =
- (Attrib.add_del_args sym_add_global sym_del_global,
-  Attrib.add_del_args sym_add_local sym_del_local);
+val trans_att = Attrib.add_del_args trans_add trans_del;
+val sym_att = Attrib.add_del_args sym_add sym_del;
 
 val _ = Context.add_setup
  [Attrib.add_attributes
-   [("trans", trans_attr, "declaration of transitivity rule"),
-    ("sym", sym_attr, "declaration of symmetry rule"),
-    ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
-      "resolution with symmetry rule")],
+   [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
+    ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
+    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
   snd o PureThy.add_thms
-   [(("", transitive_thm), [trans_add_global]),
-    (("", symmetric_thm), [sym_add_global])]];
+   [(("", transitive_thm), [Attrib.theory trans_add]),
+    (("", symmetric_thm), [Attrib.theory sym_add])]];
 
 
 
@@ -158,6 +124,8 @@
 
 (* also and finally *)
 
+val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
+
 fun calculate prep_rules final raw_rules int state =
   let
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
@@ -168,8 +136,8 @@
     fun combine ths =
       (case opt_rules of SOME rules => rules
       | NONE =>
-          (case ths of [] => NetRules.rules (#1 (get_local_rules state))
-          | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
+          (case ths of [] => NetRules.rules (#1 (get_rules state))
+          | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
       |> Seq.filter (not o projection ths);
 
diff -r cb068cfdcac8 -r 33a6f6caa617 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML	Tue Jan 10 19:33:36 2006 +0100
@@ -15,40 +15,21 @@
   val orderlist: ((int * int) * 'a) list -> 'a list
   val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
   val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list
-  val print_global_rules: theory -> unit
-  val print_local_rules: ProofContext.context -> unit
+  val print_rules: Context.generic -> unit
   val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
   val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
   val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
   val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
-  val intro_bang_global: int option -> theory attribute
-  val elim_bang_global: int option -> theory attribute
-  val dest_bang_global: int option -> theory attribute
-  val intro_global: int option -> theory attribute
-  val elim_global: int option -> theory attribute
-  val dest_global: int option -> theory attribute
-  val intro_query_global: int option -> theory attribute
-  val elim_query_global: int option -> theory attribute
-  val dest_query_global: int option -> theory attribute
-  val rule_del_global: theory attribute
-  val intro_bang_local: int option -> ProofContext.context attribute
-  val elim_bang_local: int option -> ProofContext.context attribute
-  val dest_bang_local: int option -> ProofContext.context attribute
-  val intro_local: int option -> ProofContext.context attribute
-  val elim_local: int option -> ProofContext.context attribute
-  val dest_local: int option -> ProofContext.context attribute
-  val intro_query_local: int option -> ProofContext.context attribute
-  val elim_query_local: int option -> ProofContext.context attribute
-  val dest_query_local: int option -> ProofContext.context attribute
-  val rule_del_local: ProofContext.context attribute
-  val addXIs_global: theory * thm list -> theory
-  val addXEs_global: theory * thm list -> theory
-  val addXDs_global: theory * thm list -> theory
-  val delrules_global: theory * thm list -> theory
-  val addXIs_local: ProofContext.context * thm list -> ProofContext.context
-  val addXEs_local: ProofContext.context * thm list -> ProofContext.context
-  val addXDs_local: ProofContext.context * thm list -> ProofContext.context
-  val delrules_local: ProofContext.context * thm list -> ProofContext.context
+  val intro_bang: int option -> Context.generic attribute
+  val elim_bang: int option -> Context.generic attribute
+  val dest_bang: int option -> Context.generic attribute
+  val intro: int option -> Context.generic attribute
+  val elim: int option -> Context.generic attribute
+  val dest: int option -> Context.generic attribute
+  val intro_query: int option -> Context.generic attribute
+  val elim_query: int option -> Context.generic attribute
+  val dest_query: int option -> Context.generic attribute
+  val rule_del: Context.generic attribute
 end;
 
 structure ContextRules: CONTEXT_RULES =
@@ -78,7 +59,7 @@
 val rule_indexes = distinct (map #1 rule_kinds);
 
 
-(* raw data *)
+(* context data *)
 
 type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net;
 val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty);
@@ -108,60 +89,45 @@
     else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   end;
 
-fun print_rules prt x (Rules {rules, ...}) =
-  let
-    fun prt_kind (i, b) =
-      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
-        (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
-          (sort (int_ord o pairself fst) rules));
-  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
-
-
-(* theory and proof data *)
-
-structure GlobalRulesArgs =
-struct
+structure Rules = GenericDataFun
+(
   val name = "Isar/rules";
   type T = T;
 
   val empty = make_rules ~1 [] empty_netpairs ([], []);
-  val copy = I;
   val extend = I;
 
   fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
       Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
     let
-      val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
+      val wrappers =
+        (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
       val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
           k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
       val next = ~ (length rules);
       val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
           nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
         (empty_netpairs, next upto ~1 ~~ rules);
-    in make_rules (next - 1) rules netpairs wrappers end;
-
-  val print = print_rules Display.pretty_thm_sg;
-end;
-
-structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
-val _ = Context.add_setup [GlobalRules.init];
-val print_global_rules = GlobalRules.print;
+    in make_rules (next - 1) rules netpairs wrappers end
 
-structure LocalRules = ProofDataFun
-(struct
-  val name = GlobalRulesArgs.name;
-  type T = GlobalRulesArgs.T;
-  val init = GlobalRules.get;
-  val print = print_rules ProofContext.pretty_thm;
-end);
+  fun print generic (Rules {rules, ...}) =
+    let
+      val ctxt = Context.proof_of generic;
+      fun prt_kind (i, b) =
+        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
+          (List.mapPartial (fn (_, (k, th)) =>
+              if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+            (sort (int_ord o pairself fst) rules));
+    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+);
 
-val _ = Context.add_setup [LocalRules.init];
-val print_local_rules = LocalRules.print;
+val _ = Context.add_setup [Rules.init];
+val print_rules = Rules.print;
 
 
 (* access data *)
 
-fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end;
+fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end;
 val netpair_bang = hd o netpairs;
 val netpair = hd o tl o netpairs;
 
@@ -197,15 +163,16 @@
 
 (* wrappers *)
 
-fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
-  make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers));
+fun gen_add_wrapper upd w = Context.the_theory o
+  Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+    make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)) o Context.Theory;
 
 val addSWrapper = gen_add_wrapper Library.apfst;
 val addWrapper = gen_add_wrapper Library.apsnd;
 
 
 fun gen_wrap which ctxt =
-  let val Rules {wrappers, ...} = LocalRules.get ctxt
+  let val Rules {wrappers, ...} = Rules.get (Context.Proof ctxt)
   in fold_rev fst (which wrappers) end;
 
 val Swrap = gen_wrap #1;
@@ -217,57 +184,44 @@
 
 (* add and del rules *)
 
-local
+fun rule_del (x, th) =
+  (Rules.map (del_rule th o del_rule (Tactic.make_elim th)) x, th);
 
-fun del map_data (x, th) =
-  (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, 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;
 
-fun add k view map_data opt_w =
-  (fn (x, th) => (map_data (add_rule k opt_w (view th)) x, th)) o del map_data;
+val intro_bang  = rule_add intro_bangK I;
+val elim_bang   = rule_add elim_bangK I;
+val dest_bang   = rule_add elim_bangK Tactic.make_elim;
+val intro       = rule_add introK I;
+val elim        = rule_add elimK I;
+val dest        = rule_add elimK Tactic.make_elim;
+val intro_query = rule_add intro_queryK I;
+val elim_query  = rule_add elim_queryK I;
+val dest_query  = rule_add elim_queryK Tactic.make_elim;
 
-in
+val _ = Context.add_setup
+  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
+
 
-val intro_bang_global  = add intro_bangK I GlobalRules.map;
-val elim_bang_global   = add elim_bangK I GlobalRules.map;
-val dest_bang_global   = add elim_bangK Tactic.make_elim GlobalRules.map;
-val intro_global       = add introK I GlobalRules.map;
-val elim_global        = add elimK I GlobalRules.map;
-val dest_global        = add elimK Tactic.make_elim GlobalRules.map;
-val intro_query_global = add intro_queryK I GlobalRules.map;
-val elim_query_global  = add elim_queryK I GlobalRules.map;
-val dest_query_global  = add elim_queryK Tactic.make_elim GlobalRules.map;
-val rule_del_global    = del GlobalRules.map;
+(* concrete syntax *)
+
+fun add_args a b c x = Attrib.syntax
+  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
+    >> (fn (f, n) => f n)) x;
+
+fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
 
-val intro_bang_local   = add intro_bangK I LocalRules.map;
-val elim_bang_local    = add elim_bangK I LocalRules.map;
-val dest_bang_local    = add elim_bangK Tactic.make_elim LocalRules.map;
-val intro_local        = add introK I LocalRules.map;
-val elim_local         = add elimK I LocalRules.map;
-val dest_local         = add elimK Tactic.make_elim LocalRules.map;
-val intro_query_local  = add intro_queryK I LocalRules.map;
-val elim_query_local   = add elim_queryK I LocalRules.map;
-val dest_query_local   = add elim_queryK Tactic.make_elim LocalRules.map;
-val rule_del_local     = del LocalRules.map;
+val rule_atts =
+ [("intro", Attrib.common (add_args intro_bang intro intro_query),
+    "declaration of introduction rule"),
+  ("elim", Attrib.common (add_args elim_bang elim elim_query),
+    "declaration of elimination rule"),
+  ("dest", Attrib.common (add_args dest_bang dest dest_query),
+    "declaration of destruction rule"),
+  ("rule", Attrib.common (del_args rule_del),
+    "remove declaration of intro/elim/dest rule")];
+
+val _ = Context.add_setup [Attrib.add_attributes rule_atts];
 
 end;
-
-val _ = Context.add_setup
-  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
-
-
-(* low-level modifiers *)
-
-fun modifier att (x, ths) =
-  fst (Thm.applys_attributes [att] (x, rev ths));
-
-val addXIs_global = modifier (intro_query_global NONE);
-val addXEs_global = modifier (elim_query_global NONE);
-val addXDs_global = modifier (dest_query_global NONE);
-val delrules_global = modifier rule_del_global;
-
-val addXIs_local = modifier (intro_query_local NONE);
-val addXEs_local = modifier (elim_query_local NONE);
-val addXDs_local = modifier (dest_query_local NONE);
-val delrules_local = modifier rule_del_local;
-
-end;
diff -r cb068cfdcac8 -r 33a6f6caa617 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Tue Jan 10 19:33:35 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Tue Jan 10 19:33:36 2006 +0100
@@ -8,16 +8,11 @@
 signature INDUCT_ATTRIB =
 sig
   val vars_of: term -> term list
-  val dest_global_rules: theory ->
+  val dest_rules: Context.generic ->
     {type_cases: (string * thm) list, set_cases: (string * thm) list,
       type_induct: (string * thm) list, set_induct: (string * thm) list,
       type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
-  val print_global_rules: theory -> unit
-  val dest_local_rules: Proof.context ->
-    {type_cases: (string * thm) list, set_cases: (string * thm) list,
-      type_induct: (string * thm) list, set_induct: (string * thm) list,
-      type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
-  val print_local_rules: Proof.context -> unit
+  val print_rules: Context.generic -> unit
   val lookup_casesT : Proof.context -> string -> thm option
   val lookup_casesS : Proof.context -> string -> thm option
   val lookup_inductT : Proof.context -> string -> thm option
@@ -30,18 +25,12 @@
   val find_inductS: Proof.context -> term -> thm list
   val find_coinductT: Proof.context -> typ -> thm list
   val find_coinductS: Proof.context -> term -> thm list
-  val cases_type_global: string -> theory attribute
-  val cases_set_global: string -> theory attribute
-  val cases_type_local: string -> Proof.context attribute
-  val cases_set_local: string -> Proof.context attribute
-  val induct_type_global: string -> theory attribute
-  val induct_set_global: string -> theory attribute
-  val induct_type_local: string -> Proof.context attribute
-  val induct_set_local: string -> Proof.context attribute
-  val coinduct_type_global: string -> theory attribute
-  val coinduct_set_global: string -> theory attribute
-  val coinduct_type_local: string -> Proof.context attribute
-  val coinduct_set_local: string -> Proof.context attribute
+  val cases_type: string -> Context.generic attribute
+  val cases_set: string -> Context.generic attribute
+  val induct_type: string -> Context.generic attribute
+  val induct_set: string -> Context.generic attribute
+  val coinduct_type: string -> Context.generic attribute
+  val coinduct_set: string -> Context.generic attribute
   val casesN: string
   val inductN: string
   val coinductN: string
@@ -88,7 +77,7 @@
 
 
 
-(** global and local induct data **)
+(** induct data **)
 
 (* rules *)
 
@@ -100,24 +89,23 @@
 
 fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
 
-fun pretty_rules prt kind x rs =
+fun pretty_rules ctxt kind rs =
   let val thms = map snd (NetRules.rules rs)
-  in Pretty.big_list kind (map (prt x) thms) end;
-
-fun print_all_rules prt x ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
- [pretty_rules prt "coinduct type:" x coinductT,
-  pretty_rules prt "coinduct set:" x coinductS,
-  pretty_rules prt "induct type:" x inductT,
-  pretty_rules prt "induct set:" x inductS,
-  pretty_rules prt "cases type:" x casesT,
-  pretty_rules prt "cases set:" x casesS]
- |> Pretty.chunks |> Pretty.writeln;
+  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
 
 
-(* theory data *)
+(* context data *)
 
-structure GlobalInductArgs =
-struct
+fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
+  {type_cases = NetRules.rules casesT,
+   set_cases = NetRules.rules casesS,
+   type_induct = NetRules.rules inductT,
+   set_induct = NetRules.rules inductS,
+   type_coinduct = NetRules.rules coinductT,
+   set_coinduct = NetRules.rules coinductS};
+
+structure Induct = GenericDataFun
+(
   val name = "Isar/induct";
   type T = (rules * rules) * (rules * rules) * (rules * rules);
 
@@ -125,59 +113,46 @@
     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
-  val copy = I;
+
   val extend = I;
+
   fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
       ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
 
-  fun print x = print_all_rules Display.pretty_thm_sg x;
-
-  fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
-    {type_cases = NetRules.rules casesT,
-     set_cases = NetRules.rules casesS,
-     type_induct = NetRules.rules inductT,
-     set_induct = NetRules.rules inductS,
-     type_coinduct = NetRules.rules coinductT,
-     set_coinduct = NetRules.rules coinductS};
-end;
-
-structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
-val _ = Context.add_setup [GlobalInduct.init];
-val print_global_rules = GlobalInduct.print;
-val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
+  fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
+    let val ctxt = Context.proof_of generic in
+     [pretty_rules ctxt "coinduct type:" coinductT,
+      pretty_rules ctxt "coinduct set:" coinductS,
+      pretty_rules ctxt "induct type:" inductT,
+      pretty_rules ctxt "induct set:" inductS,
+      pretty_rules ctxt "cases type:" casesT,
+      pretty_rules ctxt "cases set:" casesS]
+     |> Pretty.chunks |> Pretty.writeln
+    end
+);
 
-
-(* proof data *)
-
-structure LocalInduct = ProofDataFun
-(struct
-  val name = "Isar/induct";
-  type T = GlobalInductArgs.T;
+val _ = Context.add_setup [Induct.init];
+val print_rules = Induct.print;
+val dest_rules = dest o Induct.get;
 
-  fun init thy = GlobalInduct.get thy;
-  fun print x = print_all_rules ProofContext.pretty_thm x;
-end);
-
-val _ = Context.add_setup [LocalInduct.init];
-val print_local_rules = LocalInduct.print;
-val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
+val get_local = Induct.get o Context.Proof;
 
 
 (* access rules *)
 
-val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
-val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
-val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
-val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
-val lookup_coinductT = lookup_rule o #1 o #3 o LocalInduct.get;
-val lookup_coinductS = lookup_rule o #2 o #3 o LocalInduct.get;
+val lookup_casesT = lookup_rule o #1 o #1 o get_local;
+val lookup_casesS = lookup_rule o #2 o #1 o get_local;
+val lookup_inductT = lookup_rule o #1 o #2 o get_local;
+val lookup_inductS = lookup_rule o #2 o #2 o get_local;
+val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
+val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
 
 
 fun find_rules which how ctxt x =
-  map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
+  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
 
 val find_casesT = find_rules (#1 o #1) encode_type;
 val find_casesS = find_rules (#2 o #1) I;
@@ -192,8 +167,8 @@
 
 local
 
-fun mk_att f g h name arg =
-  let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
+fun mk_att f g name arg =
+  let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
 
 fun map1 f (x, y, z) = (f x, y, z);
 fun map2 f (x, y, z) = (x, f y, z);
@@ -211,23 +186,17 @@
 
 in
 
-val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
-val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
-val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
-val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
-val coinduct_type_global = mk_att GlobalInduct.map add_coinductT consumes0;
-val coinduct_set_global = mk_att GlobalInduct.map add_coinductS consumes1;
-
-val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
-val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
-val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
-val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
-val coinduct_type_local = mk_att LocalInduct.map add_coinductT consumes0;
-val coinduct_set_local = mk_att LocalInduct.map add_coinductS consumes1;
+val cases_type = mk_att add_casesT consumes0;
+val cases_set = mk_att add_casesS consumes1;
+val induct_type = mk_att add_inductT consumes0;
+val induct_set = mk_att add_inductS consumes1;
+val coinduct_type = mk_att add_coinductT consumes0;
+val coinduct_set = mk_att add_coinductS consumes1;
 
 end;
 
 
+
 (** concrete syntax **)
 
 val casesN = "cases";
@@ -243,29 +212,21 @@
   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   Scan.lift (Args.$$$ k) >> K "";
 
-fun attrib tyname const add_type add_set =
-  Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
+fun attrib add_type add_set =
+  Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
 
 in
 
-val cases_attr =
- (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
-  attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
-
-val induct_attr =
- (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
-  attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
-
-val coinduct_attr =
- (attrib Args.global_tyname Args.global_const coinduct_type_global coinduct_set_global,
-  attrib Args.local_tyname Args.local_const coinduct_type_local coinduct_set_local);
+val cases_att = attrib cases_type cases_set;
+val induct_att = attrib induct_type induct_set;
+val coinduct_att = attrib coinduct_type coinduct_set;
 
 end;
 
 val _ = Context.add_setup
  [Attrib.add_attributes
-  [(casesN, cases_attr, "declaration of cases rule for type or set"),
-   (inductN, induct_attr, "declaration of induction rule for type or set"),
-   (coinductN, coinduct_attr, "declaration of coinduction rule for type or set")]];
+  [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
+   (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
+   (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]];
 
 end;