--- a/src/HOL/Tools/datatype_package.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Jan 10 19:34:04 2006 +0100
@@ -365,10 +365,10 @@
fun proj i = ProjectRule.project induction (i + 1);
fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
- [(("", proj index), [InductAttrib.induct_type_global name]),
- (("", exhaustion), [InductAttrib.cases_type_global name])];
+ [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]),
+ (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])];
fun unnamed_rule i =
- (("", proj i), [Drule.kind_internal, InductAttrib.induct_type_global ""]);
+ (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]);
in
PureThy.add_thms
(List.concat (map named_rules infos) @
--- a/src/HOL/Tools/inductive_package.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Jan 10 19:34:04 2006 +0100
@@ -435,12 +435,12 @@
thy
|> Theory.parent_path
|> Theory.add_path (Sign.base_name name)
- |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])] |> snd
+ |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
|> Theory.restore_naming thy;
val cases_specs = if no_elim then [] else map2 cases_spec names elims;
val induct_att =
- if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
+ Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
val induct_specs =
if no_induct then I
else
--- a/src/HOL/Tools/record_package.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Tue Jan 10 19:34:04 2006 +0100
@@ -1215,8 +1215,8 @@
(* attributes *)
fun case_names_fields x = RuleCases.case_names ["fields"] x;
-fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
-fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
+fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)];
+fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
(* tactics *)
--- a/src/HOL/Tools/typedef_package.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Tue Jan 10 19:34:04 2006 +0100
@@ -176,13 +176,17 @@
((Rep_name ^ "_inject", make Rep_inject), []),
((Abs_name ^ "_inject", make Abs_inject), []),
((Rep_name ^ "_cases", make Rep_cases),
- [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
+ [RuleCases.case_names [Rep_name],
+ Attrib.theory (InductAttrib.cases_set full_name)]),
((Abs_name ^ "_cases", make Abs_cases),
- [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
+ [RuleCases.case_names [Abs_name],
+ Attrib.theory (InductAttrib.cases_type full_tname)]),
((Rep_name ^ "_induct", make Rep_induct),
- [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
+ [RuleCases.case_names [Rep_name],
+ Attrib.theory (InductAttrib.induct_set full_name)]),
((Abs_name ^ "_induct", make Abs_induct),
- [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
+ [RuleCases.case_names [Abs_name],
+ Attrib.theory (InductAttrib.induct_type full_tname)])])
||> Theory.parent_path;
val result = {type_definition = type_definition, set_def = set_def,
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
--- a/src/Provers/classical.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/Provers/classical.ML Tue Jan 10 19:34:04 2006 +0100
@@ -968,7 +968,7 @@
val haz_dest_global = change_global_cs (op addDs);
val haz_elim_global = change_global_cs (op addEs);
val haz_intro_global = change_global_cs (op addIs);
-val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
+val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
val safe_dest_local = change_local_cs (op addSDs);
val safe_elim_local = change_local_cs (op addSEs);
@@ -976,7 +976,7 @@
val haz_dest_local = change_local_cs (op addDs);
val haz_elim_local = change_local_cs (op addEs);
val haz_intro_local = change_local_cs (op addIs);
-val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
+val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
(* tactics referring to the implicit claset *)
@@ -1019,16 +1019,16 @@
val setup_attrs = Attrib.add_attributes
[("swapped", (swapped, swapped), "classical swap of introduction rule"),
(destN,
- (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global,
- add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local),
+ (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
+ add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
"declaration of destruction rule"),
(elimN,
- (add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global,
- add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local),
+ (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
+ add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
"declaration of elimination rule"),
(introN,
- (add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global,
- add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local),
+ (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
+ add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
"declaration of introduction rule"),
(ruleN, (del_rule rule_del_global, del_rule rule_del_local),
"remove declaration of intro/elim/dest rule")];
--- a/src/Pure/Isar/obtain.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/Pure/Isar/obtain.ML Tue Jan 10 19:34:04 2006 +0100
@@ -134,7 +134,8 @@
|> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [([thesisN], NONE)]
- |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
+ |> Proof.assume_i
+ [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
--- a/src/ZF/Tools/inductive_package.ML Tue Jan 10 19:33:42 2006 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Jan 10 19:34:04 2006 +0100
@@ -514,8 +514,9 @@
val ([induct', mutual_induct'], thy') =
thy
- |> PureThy.add_thms [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
- (("mutual_induct", mutual_induct), [case_names])];
+ |> PureThy.add_thms [((co_prefix ^ "induct", induct),
+ [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]),
+ (("mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -536,7 +537,7 @@
|> PureThy.add_thms
[(("bnd_mono", bnd_mono), []),
(("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, InductAttrib.cases_set_global big_rec_name])]
+ (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];