--- a/src/HOL/Import/hol4rews.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML Sat Jan 21 23:02:14 2006 +0100
@@ -258,15 +258,16 @@
val hol4_debug = ref false
fun message s = if !hol4_debug then writeln s else ()
-fun add_hol4_rewrite (thy,th) =
+fun add_hol4_rewrite (context, th) =
let
+ val thy = Context.the_theory context;
val _ = message "Adding HOL4 rewrite"
val th1 = th RS eq_reflection
val current_rews = HOL4Rewrites.get thy
val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
val updated_thy = HOL4Rewrites.put new_rews thy
in
- (updated_thy,th1)
+ (Context.Theory updated_thy,th1)
end;
fun ignore_hol4 bthy bthm thy =
@@ -775,8 +776,5 @@
ImportSegment.init #>
initial_maps #>
Attrib.add_attributes
- [("hol4rew",
- (Attrib.no_args add_hol4_rewrite,
- Attrib.no_args Attrib.undef_local_attribute),
- "HOL4 rewrite rule")]
+ [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
end
--- a/src/HOL/Import/proof_kernel.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sat Jan 21 23:02:14 2006 +0100
@@ -1988,7 +1988,7 @@
val thy1 = foldr (fn(name,thy)=>
snd (get_defname thyname name thy)) thy1 names
fun new_name name = fst (get_defname thyname name thy1)
- val (thy',res) = SpecificationPackage.add_specification_i NONE
+ val (thy',res) = SpecificationPackage.add_specification NONE
(map (fn name => (new_name name,name,false)) names)
(thy1,th)
val res' = Drule.freeze_all res
--- a/src/HOL/Import/shuffler.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Import/shuffler.ML Sat Jan 21 23:02:14 2006 +0100
@@ -24,7 +24,7 @@
val print_shuffles: theory -> unit
val add_shuffle_rule: thm -> theory -> theory
- val shuffle_attr: theory attribute
+ val shuffle_attr: attribute
val setup : theory -> theory
end
@@ -682,7 +682,7 @@
else ShuffleData.put (thm::shuffles) thy
end
-fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm)
+val shuffle_attr = Thm.declaration_attribute (Context.map_theory o add_shuffle_rule);
val setup =
Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
@@ -693,6 +693,6 @@
add_shuffle_rule imp_comm #>
add_shuffle_rule Drule.norm_hhf_eq #>
add_shuffle_rule Drule.triv_forall_equality #>
- Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]
+ Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
end
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -19,7 +19,7 @@
sig
val prove_casedist_thms : string list ->
DatatypeAux.descr list -> (string * sort) list -> thm ->
- theory attribute list -> theory -> thm list * theory
+ attribute list -> theory -> thm list * theory
val prove_primrec_thms : bool -> string list ->
DatatypeAux.descr list -> (string * sort) list ->
DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
--- a/src/HOL/Tools/datatype_aux.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Sat Jan 21 23:02:14 2006 +0100
@@ -15,10 +15,10 @@
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
- val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
+ val store_thmss_atts : string -> string list -> attribute list list -> thm list list
-> theory -> thm list list * theory
val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
- val store_thms_atts : string -> string list -> theory attribute list list -> thm list
+ val store_thms_atts : string -> string list -> attribute list list -> thm list
-> theory -> thm list * theory
val store_thms : string -> string list -> thm list -> theory -> thm list * theory
--- a/src/HOL/Tools/datatype_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -39,8 +39,8 @@
induction : thm,
size : thm list,
simps : thm list} * theory
- val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
- (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
+ val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
+ (thm list * attribute list) list list -> (thm list * attribute list) ->
theory ->
{distinct : thm list list,
inject : thm list list,
@@ -350,10 +350,10 @@
weak_case_congs cong_att =
(snd o PureThy.add_thmss [(("simps", simps), []),
(("", List.concat case_thms @ size_thms @
- List.concat distinct @ rec_thms), [Attrib.theory Simplifier.simp_add]),
+ List.concat distinct @ rec_thms), [Simplifier.simp_add]),
(("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
- (("", List.concat inject), [Attrib.theory iff_add]),
- (("", map name_notE (List.concat distinct)), [Attrib.theory (Classical.safe_elim NONE)]),
+ (("", List.concat inject), [iff_add]),
+ (("", map name_notE (List.concat distinct)), [Classical.safe_elim NONE]),
(("", weak_case_congs), [cong_att])]);
@@ -365,10 +365,10 @@
fun proj i = ProjectRule.project induction (i + 1);
fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
- [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]),
- (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])];
+ [(("", proj index), [InductAttrib.induct_type name]),
+ (("", exhaustion), [InductAttrib.cases_type name])];
fun unnamed_rule i =
- (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]);
+ (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
in
PureThy.add_thms
(List.concat (map named_rules infos) @
@@ -747,7 +747,7 @@
|> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
|> Theory.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Attrib.theory Simplifier.cong_add)
+ weak_case_congs Simplifier.cong_add
|> put_datatypes (fold Symtab.update dt_infos dt_info)
|> add_cases_induct dt_infos induct
|> Theory.parent_path
@@ -806,7 +806,7 @@
|> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
|> Theory.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
+ weak_case_congs (Simplifier.attrib (op addcongs))
|> put_datatypes (fold Symtab.update dt_infos dt_info)
|> add_cases_induct dt_infos induct
|> Theory.parent_path
@@ -913,7 +913,7 @@
val thy11 = thy10 |>
Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |>
+ weak_case_congs (Simplifier.attrib (op addcongs)) |>
put_datatypes (fold Symtab.update dt_infos dt_info) |>
add_cases_induct dt_infos induction' |>
Theory.parent_path |>
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -15,7 +15,7 @@
sig
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> DatatypeAux.descr list -> (string * sort) list ->
- (string * mixfix) list -> (string * mixfix) list list -> theory attribute
+ (string * mixfix) list -> (string * mixfix) list list -> attribute
-> theory -> (thm list list * thm list list * thm list list *
DatatypeAux.simproc_dist list * thm) * theory
end;
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Sat Jan 21 23:02:14 2006 +0100
@@ -7,7 +7,7 @@
signature INDUCTIVE_CODEGEN =
sig
- val add : string option -> theory attribute
+ val add : string option -> attribute
val setup : theory -> theory
end;
@@ -45,7 +45,7 @@
fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
-fun add optmod (p as (thy, thm)) =
+fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
let
val {intros, graph, eqns} = CodegenData.get thy;
fun thyname_of s = (case optmod of
@@ -54,22 +54,22 @@
_ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
Const (s, _) =>
let val cs = foldr add_term_consts [] (prems_of thm)
- in (CodegenData.put
+ in CodegenData.put
{intros = intros |>
Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]),
graph = foldr (uncurry (Graph.add_edge o pair s))
(Library.foldl add_node (graph, s :: cs)) cs,
- eqns = eqns} thy, thm)
+ eqns = eqns} thy
end
- | _ => (warn thm; p))
+ | _ => (warn thm; thy))
| _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
Const (s, _) =>
- (CodegenData.put {intros = intros, graph = graph,
+ CodegenData.put {intros = intros, graph = graph,
eqns = eqns |> Symtab.update
- (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
- | _ => (warn thm; p))
- | _ => (warn thm; p))
- end;
+ (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy
+ | _ => (warn thm; thy))
+ | _ => (warn thm; thy))
+ end));
fun get_clauses thy s =
let val {intros, graph, ...} = CodegenData.get thy
--- a/src/HOL/Tools/inductive_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -38,16 +38,16 @@
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
val the_mk_cases: theory -> string -> string -> thm
val print_inductives: theory -> unit
- val mono_add_global: theory attribute
- val mono_del_global: theory attribute
+ val mono_add: attribute
+ val mono_del: attribute
val get_monos: theory -> thm list
val inductive_forall_name: string
val inductive_forall_def: thm
val rulify: thm -> thm
val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
- val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
+ val inductive_cases_i: ((bstring * attribute list) * term list) list -> theory -> theory
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
- ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
+ ((bstring * term) * attribute list) list -> thm list -> theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
val add_inductive: bool -> bool -> string list ->
@@ -128,7 +128,7 @@
(** monotonicity rules **)
val get_monos = #2 o InductiveData.get;
-fun map_monos f = InductiveData.map (Library.apsnd f);
+val map_monos = Context.map_theory o InductiveData.map o Library.apsnd;
fun mk_mono thm =
let
@@ -148,12 +148,8 @@
(* attributes *)
-fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
-fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
-
-val mono_attr =
- (Attrib.add_del_args mono_add_global mono_del_global,
- Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
+val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono);
+val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono);
@@ -435,12 +431,11 @@
thy
|> Theory.parent_path
|> Theory.add_path (Sign.base_name name)
- |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
+ |> PureThy.add_thms [(("cases", elim), [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 =
- Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
+ val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
val induct_specs =
if no_induct then I
else
@@ -577,7 +572,7 @@
((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
-val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
+val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
@@ -852,7 +847,7 @@
fun read_rule s = Thm.read_cterm thy (s, propT)
handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
- val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
+ val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs;
val (cs', intr_ts') = unify_consts thy cs intr_ts;
val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
@@ -871,7 +866,8 @@
InductiveData.init #>
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
"dynamic case analysis on sets")] #>
- Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
+ Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
+ "declaration of monotonicity rule")];
(* outer syntax *)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Jan 21 23:02:14 2006 +0100
@@ -467,7 +467,7 @@
Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
end
-fun rlz_attrib arg (thy, thm) =
+fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
let
fun err () = error "ind_realizer: bad rule";
val sets =
@@ -476,21 +476,19 @@
| xs => map (set_of o fst o HOLogic.dest_imp) xs)
handle TERM _ => err () | Empty => err ();
in
- (add_ind_realizers (hd sets) (case arg of
+ add_ind_realizers (hd sets)
+ (case arg of
NONE => sets | SOME NONE => []
| SOME (SOME sets') => sets \\ sets')
- thy, thm)
- end;
+ end);
-val rlz_attrib_global = Attrib.syntax
+val ind_realizer = Attrib.syntax
((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 Args.global_const))) >> rlz_attrib);
+ Scan.repeat1 Args.const))) >> rlz_attrib);
val setup =
- Attrib.add_attributes [("ind_realizer",
- (rlz_attrib_global, K Attrib.undef_local_attribute),
- "add realizers for inductive set")];
+ Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
end;
--- a/src/HOL/Tools/primrec_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -10,7 +10,7 @@
val quiet_mode: bool ref
val add_primrec: string -> ((bstring * string) * Attrib.src list) list
-> theory -> theory * thm list
- val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
+ val add_primrec_i: string -> ((bstring * term) * attribute list) list
-> theory -> theory * thm list
end;
@@ -258,7 +258,7 @@
val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
|> (snd o PureThy.add_thmss [(("simps", simps'),
- [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
+ [Simplifier.simp_add, RecfunCodegen.add NONE])])
|> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
|> Theory.parent_path
in
@@ -270,7 +270,7 @@
let
val sign = Theory.sign_of thy;
val ((names, strings), srcss) = apfst split_list (split_list eqns);
- val atts = map (map (Attrib.global_attribute thy)) srcss;
+ val atts = map (map (Attrib.attribute thy)) srcss;
val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT))
handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
--- a/src/HOL/Tools/recdef_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -11,24 +11,23 @@
val print_recdefs: theory -> unit
val get_recdef: theory -> string
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
- val simp_add: Context.generic attribute
- val simp_del: Context.generic attribute
- val cong_add: Context.generic attribute
- val cong_del: Context.generic attribute
- val wf_add: Context.generic attribute
- val wf_del: Context.generic attribute
+ val simp_add: attribute
+ val simp_del: attribute
+ val cong_add: attribute
+ val cong_del: attribute
+ val wf_add: attribute
+ val wf_del: attribute
val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
Attrib.src option -> theory -> theory
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
+ val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
-> theory -> theory * {induct_rules: thm}
- val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
+ val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
-> theory -> theory * {induct_rules: thm}
val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
- val recdef_tc_i: bstring * theory attribute list -> string -> int option
- -> theory -> Proof.state
+ val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
val setup: theory -> theory
end;
@@ -148,7 +147,7 @@
fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
| map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
-fun attrib f = Attrib.declaration (map_hints o f);
+fun attrib f = Thm.declaration_attribute (map_hints o f);
val simp_add = attrib (map_simps o Drule.add_rule);
val simp_del = attrib (map_simps o Drule.del_rule);
@@ -165,15 +164,15 @@
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
- Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
- Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
- Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
- Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
- Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
- Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
- Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
- Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
+ Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
+ Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
+ Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
+ Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
+ Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
+ Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
+ Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
+ Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
Clasimp.clasimp_modifiers;
@@ -223,8 +222,7 @@
tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
congs wfs name R eqs;
val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
- val simp_att = if null tcs then
- [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
+ val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else [];
val ((simps' :: rules', [induct']), thy) =
thy
@@ -239,7 +237,7 @@
|> Theory.parent_path;
in (thy, result) end;
-val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints;
+val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
@@ -284,7 +282,7 @@
" in recdef definition of " ^ quote name);
in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
-val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
+val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
val recdef_tc_i = gen_recdef_tc (K I) (K I);
@@ -297,12 +295,9 @@
GlobalRecdefData.init #>
LocalRecdefData.init #>
Attrib.add_attributes
- [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
- "declaration of recdef simp rule"),
- (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
- "declaration of recdef cong rule"),
- (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
- "declaration of recdef wf rule")];
+ [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
+ (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
+ (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
(* outer syntax *)
--- a/src/HOL/Tools/recfun_codegen.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Sat Jan 21 23:02:14 2006 +0100
@@ -7,8 +7,8 @@
signature RECFUN_CODEGEN =
sig
- val add: string option -> theory attribute
- val del: theory attribute
+ val add: string option -> attribute
+ val del: attribute
val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
val get_thm_equations: theory -> string * typ -> (thm list * typ) option
val setup: theory -> theory
@@ -38,25 +38,25 @@
fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
string_of_thm thm);
-fun add optmod (p as (thy, thm)) =
+fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
let
val tab = CodegenData.get thy;
val (s, _) = const_of (prop_of thm);
in
if Pattern.pattern (lhs_of thm) then
- (CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy, thm)
- else (warn thm; p)
- end handle TERM _ => (warn thm; p);
+ CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy
+ else (warn thm; thy)
+ end handle TERM _ => (warn thm; thy)));
-fun del (p as (thy, thm)) =
+val del = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
let
val tab = CodegenData.get thy;
val (s, _) = const_of (prop_of thm);
in case Symtab.lookup tab s of
- NONE => p
- | SOME thms => (CodegenData.put (Symtab.update (s,
- gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
- end handle TERM _ => (warn thm; p);
+ NONE => thy
+ | SOME thms =>
+ CodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
+ end handle TERM _ => (warn thm; thy)));
fun del_redundant thy eqs [] = eqs
| del_redundant thy eqs (eq :: eqs') =
--- a/src/HOL/Tools/record_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Jan 21 23:02:14 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, Attrib.theory (InductAttrib.induct_type name)];
-fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
+fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
+fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
(* tactics *)
@@ -1993,8 +1993,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
- (("iffs",iffs), [Attrib.theory iff_add])]
+ [(("simps", sel_upd_simps), [Simplifier.simp_add]),
+ (("iffs",iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
|> add_record_equalities extension_id equality'
--- a/src/HOL/Tools/res_axioms.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sat Jan 21 23:02:14 2006 +0100
@@ -484,18 +484,15 @@
(*Conjoin a list of clauses to recreate a single theorem*)
val conj_rule = foldr1 conj2_rule;
-fun skolem_global_fun (thy, th) =
- let val name = Thm.name_of_thm th
- val (cls,thy') = skolem_cache_thm ((name,th), thy)
- in (thy', conj_rule cls) end;
-
-val skolem_global = Attrib.no_args skolem_global_fun;
-
-fun skolem_local x = Attrib.no_args (Attrib.rule (K (conj_rule o skolem_thm))) x;
+fun skolem (Context.Theory thy, th) =
+ let
+ val name = Thm.name_of_thm th
+ val (cls, thy') = skolem_cache_thm ((name, th), thy)
+ in (Context.Theory thy', conj_rule cls) end
+ | skolem (context, th) = (context, conj_rule (skolem_thm th));
val setup_attrs = Attrib.add_attributes
- [("skolem", (skolem_global, skolem_local),
- "skolemization of a theorem")];
+ [("skolem", Attrib.no_args skolem, "skolemization of a theorem")];
val setup = clause_cache_setup #> setup_attrs;
--- a/src/HOL/Tools/split_rule.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/split_rule.ML Sat Jan 21 23:02:14 2006 +0100
@@ -136,13 +136,13 @@
fun split_format x = Attrib.syntax
(Scan.lift (Args.parens (Args.$$$ "complete"))
- >> K (Attrib.rule (K complete_split_rule)) ||
+ >> K (Thm.rule_attribute (K complete_split_rule)) ||
Args.and_list1 (Scan.lift (Scan.repeat Args.name))
- >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
+ >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
val setup =
Attrib.add_attributes
- [("split_format", (split_format, split_format),
+ [("split_format", split_format,
"split pair-typed subterms in premises, or function arguments")];
end;
--- a/src/HOL/Tools/typedef_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -150,8 +150,8 @@
else
(NONE, thy);
- fun typedef_result (theory, nonempty) =
- theory
+ fun typedef_result (context, nonempty) =
+ Context.the_theory context
|> put_typedef newT oldT (full Abs_name) (full Rep_name)
|> add_typedecls [(t, vs, mx)]
|> Theory.add_consts_i
@@ -176,23 +176,19 @@
((Rep_name ^ "_inject", make Rep_inject), []),
((Abs_name ^ "_inject", make Abs_inject), []),
((Rep_name ^ "_cases", make Rep_cases),
- [RuleCases.case_names [Rep_name],
- Attrib.theory (InductAttrib.cases_set full_name)]),
+ [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]),
((Abs_name ^ "_cases", make Abs_cases),
- [RuleCases.case_names [Abs_name],
- Attrib.theory (InductAttrib.cases_type full_tname)]),
+ [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]),
((Rep_name ^ "_induct", make Rep_induct),
- [RuleCases.case_names [Rep_name],
- Attrib.theory (InductAttrib.induct_set full_name)]),
+ [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
((Abs_name ^ "_induct", make Abs_induct),
- [RuleCases.case_names [Abs_name],
- Attrib.theory (InductAttrib.induct_type full_tname)])])
+ [RuleCases.case_names [Abs_name], 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,
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
- in ((theory'', type_definition), result) end);
+ in ((Context.Theory theory'', type_definition), result) end);
(* errors *)
@@ -220,7 +216,7 @@
(*test theory errors now!*)
val test_thy = Theory.copy thy;
- val _ = (test_thy,
+ val _ = (Context.Theory test_thy,
setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
in (cset, goal, goal_pat, typedef_result) end
@@ -239,7 +235,8 @@
val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
- val ((thy', _), result) = (thy, non_empty) |> typedef_result;
+ val (thy', result) =
+ (Context.Theory thy, non_empty) |> typedef_result |>> (Context.the_theory o fst);
in (thy', result) end;
in
--- a/src/HOL/arith_data.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/arith_data.ML Sat Jan 21 23:02:14 2006 +0100
@@ -223,8 +223,9 @@
fun print _ _ = ();
end);
-fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
- {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
+val arith_split_add = Thm.declaration_attribute (fn thm =>
+ Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
+ {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger})));
fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
{splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
@@ -584,7 +585,5 @@
Method.add_methods
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
"decide linear arithmethic")] #>
- Attrib.add_attributes [("arith_split",
- (Attrib.no_args arith_split_add,
- Attrib.no_args Attrib.undef_local_attribute),
+ Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
"declaration of split rules for arithmetic procedure")];
--- a/src/HOLCF/domain/theorems.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Jan 21 23:02:14 2006 +0100
@@ -368,7 +368,7 @@
("inverts" , inverts ),
("injects" , injects ),
("copy_rews", copy_rews)])))
- |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
+ |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add])])
|> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
end; (* let *)
--- a/src/HOLCF/fixrec_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOLCF/fixrec_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -7,14 +7,10 @@
signature FIXREC_PACKAGE =
sig
- val add_fixrec: bool -> ((string * Attrib.src list) * string) list list
- -> theory -> theory
- val add_fixrec_i: bool -> ((string * theory attribute list) * term) list list
- -> theory -> theory
- val add_fixpat: (string * Attrib.src list) * string list
- -> theory -> theory
- val add_fixpat_i: (string * theory attribute list) * term list
- -> theory -> theory
+ val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
+ val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
+ val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
@@ -250,7 +246,7 @@
val (simp_thms, thy'') = PureThy.add_thms simps thy';
val simp_names = map (fn name => name^"_simps") cnames;
- val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
+ val simp_attribute = rpair [Simplifier.simp_add];
val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
in
(snd o PureThy.add_thmss simps') thy''
@@ -258,7 +254,7 @@
else thy'
end;
-val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.global_attribute;
+val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
@@ -286,7 +282,7 @@
(snd o PureThy.add_thmss [((name, simps), atts)]) thy
end;
-val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
+val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
--- a/src/HOLCF/pcpodef_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -144,8 +144,9 @@
||> Theory.parent_path;
in (theory', defs) end;
- fun pcpodef_result (theory, UUmem_admissible) =
+ fun pcpodef_result (context, UUmem_admissible) =
let
+ val theory = Context.the_theory context;
val UUmem = UUmem_admissible RS conjunct1;
val admissible = UUmem_admissible RS conjunct2;
in
@@ -153,18 +154,19 @@
|> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
|> make_cpo admissible
|> make_pcpo UUmem
- |> (fn (theory', (type_def, _, _)) => (theory', type_def))
+ |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
end;
- fun cpodef_result (theory, nonempty_admissible) =
+ fun cpodef_result (context, nonempty_admissible) =
let
+ val theory = Context.the_theory context;
val nonempty = nonempty_admissible RS conjunct1;
val admissible = nonempty_admissible RS conjunct2;
in
theory
|> make_po (Tactic.rtac nonempty 1)
|> make_cpo admissible
- |> (fn (theory', (type_def, _, _)) => (theory', type_def))
+ |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
end;
in (goal, if pcpo then pcpodef_result else cpodef_result) end
--- a/src/Provers/clasimp.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Provers/clasimp.ML Sat Jan 21 23:02:14 2006 +0100
@@ -56,12 +56,12 @@
val fast_simp_tac: clasimpset -> int -> tactic
val slow_simp_tac: clasimpset -> int -> tactic
val best_simp_tac: clasimpset -> int -> tactic
- val attrib: (clasimpset * thm list -> clasimpset) -> Context.generic attribute
+ val attrib: (clasimpset * thm list -> clasimpset) -> attribute
val get_local_clasimpset: Proof.context -> clasimpset
val local_clasimpset_of: Proof.context -> clasimpset
- val iff_add: Context.generic attribute
- val iff_add': Context.generic attribute
- val iff_del: Context.generic attribute
+ val iff_add: attribute
+ val iff_add': attribute
+ val iff_del: attribute
val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val setup: theory -> theory
@@ -151,7 +151,7 @@
end;
fun modifier att (x, ths) =
- fst (Thm.applys_attributes [att] (x, rev ths));
+ fst (foldl_map (Library.apply [att]) (x, rev ths));
val addXIs = modifier (ContextRules.intro_query NONE);
val addXEs = modifier (ContextRules.elim_query NONE);
@@ -265,7 +265,7 @@
(* attributes *)
-fun attrib f = Attrib.declaration (fn th =>
+fun attrib f = Thm.declaration_attribute (fn th =>
fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
| Context.Proof ctxt =>
let
@@ -295,10 +295,9 @@
val iffN = "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon
- >> K ((I, Attrib.context iff_add): Method.modifier),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, Attrib.context iff_add'),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (I, Attrib.context iff_del)];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
+ Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
+ Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
@@ -328,7 +327,7 @@
val setup =
(Attrib.add_attributes
- [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")] #>
+ [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
--- a/src/Provers/classical.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Provers/classical.ML Sat Jan 21 23:02:14 2006 +0100
@@ -143,13 +143,13 @@
val print_local_claset: Proof.context -> unit
val get_local_claset: Proof.context -> claset
val put_local_claset: claset -> Proof.context -> Proof.context
- val safe_dest: int option -> Context.generic attribute
- val safe_elim: int option -> Context.generic attribute
- val safe_intro: int option -> Context.generic attribute
- val haz_dest: int option -> Context.generic attribute
- val haz_elim: int option -> Context.generic attribute
- val haz_intro: int option -> Context.generic attribute
- val rule_del: Context.generic attribute
+ val safe_dest: int option -> attribute
+ val safe_elim: int option -> attribute
+ val safe_intro: int option -> attribute
+ val haz_dest: int option -> attribute
+ val haz_elim: int option -> attribute
+ val haz_intro: int option -> attribute
+ val rule_del: attribute
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
@@ -949,7 +949,7 @@
(* attributes *)
-fun attrib f = Attrib.declaration (fn th =>
+fun attrib f = Thm.declaration_attribute (fn th =>
fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
| Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
@@ -989,14 +989,14 @@
val ruleN = "rule";
val setup_attrs = Attrib.add_attributes
- [("swapped", Attrib.common swapped, "classical swap of introduction rule"),
- (destN, Attrib.common (ContextRules.add_args safe_dest haz_dest ContextRules.dest_query),
+ [("swapped", swapped, "classical swap of introduction rule"),
+ (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
"declaration of Classical destruction rule"),
- (elimN, Attrib.common (ContextRules.add_args safe_elim haz_elim ContextRules.elim_query),
+ (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
"declaration of Classical elimination rule"),
- (introN, Attrib.common (ContextRules.add_args safe_intro haz_intro ContextRules.intro_query),
+ (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
"declaration of Classical introduction rule"),
- (ruleN, Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
+ (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
@@ -1044,13 +1044,13 @@
(* automatic methods *)
val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context (safe_dest NONE)): Method.modifier),
- Args.$$$ destN -- Args.colon >> K (I, Attrib.context (haz_dest NONE)),
- Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context (safe_elim NONE)),
- Args.$$$ elimN -- Args.colon >> K (I, Attrib.context (haz_elim NONE)),
- Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context (safe_intro NONE)),
- Args.$$$ introN -- Args.colon >> K (I, Attrib.context (haz_intro NONE)),
- Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
+ [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
+ Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
+ Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
+ Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
+ Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
+ Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
+ Args.del -- Args.colon >> K (I, rule_del)];
fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
--- a/src/Provers/splitter.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Provers/splitter.ML Sat Jan 21 23:02:14 2006 +0100
@@ -32,8 +32,8 @@
val delsplits : simpset * thm list -> simpset
val Addsplits : thm list -> unit
val Delsplits : thm list -> unit
- val split_add: Context.generic attribute
- val split_del: Context.generic attribute
+ val split_add: attribute
+ val split_del: attribute
val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
val setup: theory -> theory
end;
@@ -443,9 +443,9 @@
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
- Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
- Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
+ [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
+ Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
+ Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
fun split_meth src =
Method.syntax Attrib.local_thms src
@@ -456,8 +456,7 @@
val setup =
(Attrib.add_attributes
- [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
- "declaration of case split rule")] #>
+ [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
Method.add_methods [(splitN, split_meth, "apply case split rule")]);
end;
--- a/src/Pure/Isar/args.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/args.ML Sat Jan 21 23:02:14 2006 +0100
@@ -8,8 +8,8 @@
signature ARGS =
sig
- datatype value = Name of string | Typ of typ | Term of term | Fact of thm list |
- Attribute of Context.generic attribute
+ datatype value =
+ Name of string | Typ of typ | Term of term | Fact of thm list | Attribute of attribute
type T
val string_of: T -> string
val mk_ident: string * Position.T -> T
@@ -20,7 +20,7 @@
val mk_typ: typ -> T
val mk_term: term -> T
val mk_fact: thm list -> T
- val mk_attribute: Context.generic attribute -> T
+ val mk_attribute: attribute -> T
val stopper: T * (T -> bool)
val not_eof: T -> bool
type src
@@ -64,7 +64,7 @@
val internal_typ: T list -> typ * T list
val internal_term: T list -> term * T list
val internal_fact: T list -> thm list * T list
- val internal_attribute: T list -> Context.generic attribute * T list
+ val internal_attribute: T list -> attribute * T list
val named_name: (string -> string) -> T list -> string * T list
val named_typ: (string -> typ) -> T list -> typ * T list
val named_term: (string -> term) -> T list -> term * T list
@@ -118,7 +118,7 @@
Typ of typ |
Term of term |
Fact of thm list |
- Attribute of Context.generic attribute;
+ Attribute of attribute;
datatype slot =
Empty |
--- a/src/Pure/Isar/calculation.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/calculation.ML Sat Jan 21 23:02:14 2006 +0100
@@ -9,11 +9,11 @@
sig
val print_rules: Context.generic -> unit
val get_calculation: Proof.state -> thm list option
- 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 trans_add: attribute
+ val trans_del: attribute
+ val sym_add: attribute
+ val sym_del: attribute
+ val symmetric: 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
@@ -60,9 +60,8 @@
val calculationN = "calculation";
fun put_calculation 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.level #-> (fn lev => Proof.map_context (Context.proof_map
+ (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
#> Proof.put_thms (calculationN, calc);
@@ -71,20 +70,20 @@
(* add/del rules *)
-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 = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
+val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
val sym_add =
- Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
+ Thm.declaration_attribute (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)
+ Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
#> ContextRules.rule_del;
(* symmetric *)
-val symmetric = Attrib.rule (fn x => fn th =>
+val symmetric = Thm.rule_attribute (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])
@@ -98,12 +97,12 @@
val _ = Context.add_setup
(Attrib.add_attributes
- [("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")] #>
+ [("trans", trans_att, "declaration of transitivity rule"),
+ ("sym", sym_att, "declaration of symmetry rule"),
+ ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
PureThy.add_thms
- [(("", transitive_thm), [Attrib.theory trans_add]),
- (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
+ [(("", transitive_thm), [trans_add]),
+ (("", symmetric_thm), [sym_add])] #> snd);
--- a/src/Pure/Isar/constdefs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/constdefs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -13,7 +13,7 @@
((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
theory -> theory
val add_constdefs_i: (string * typ option) list *
- ((bstring * typ option * mixfix) option * ((bstring * theory attribute list) * term)) list ->
+ ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
theory -> theory
end;
@@ -66,7 +66,7 @@
in Pretty.writeln (Specification.pretty_consts ctxt decls); thy' end;
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
- ProofContext.read_term_legacy Attrib.global_attribute;
+ ProofContext.read_term_legacy Attrib.attribute;
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
end;
--- a/src/Pure/Isar/context_rules.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Sat Jan 21 23:02:14 2006 +0100
@@ -2,8 +2,8 @@
ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
-Declarations of intro/elim/dest rules in Pure; see
-Provers/classical.ML for a more specialized version of the same idea.
+Declarations of intro/elim/dest rules in Pure (see also
+Provers/classical.ML for a more specialized version of the same idea).
*)
signature CONTEXT_RULES =
@@ -20,18 +20,19 @@
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: 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
- val add_args: (int option -> 'a attribute) -> (int option -> 'a attribute) ->
- (int option -> 'a attribute) -> Attrib.src -> 'a attribute
+ val intro_bang: int option -> attribute
+ val elim_bang: int option -> attribute
+ val dest_bang: int option -> attribute
+ val intro: int option -> attribute
+ val elim: int option -> attribute
+ val dest: int option -> attribute
+ val intro_query: int option -> attribute
+ val elim_query: int option -> attribute
+ val dest_query: int option -> attribute
+ val rule_del: attribute
+ val add_args:
+ (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
+ Attrib.src -> attribute
end;
structure ContextRules: CONTEXT_RULES =
@@ -166,7 +167,7 @@
(* wrappers *)
fun gen_add_wrapper upd w =
- Context.map_theory (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+ Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
val addSWrapper = gen_add_wrapper Library.apfst;
@@ -203,7 +204,7 @@
val dest_query = rule_add elim_queryK Tactic.make_elim;
val _ = Context.add_setup
- (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
+ (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
(* concrete syntax *)
@@ -213,13 +214,10 @@
>> (fn (f, n) => f n)) x;
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 (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
+ [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
+ ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
+ ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
+ ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
val _ = Context.add_setup (Attrib.add_attributes rule_atts);
--- a/src/Pure/Isar/induct_attrib.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Sat Jan 21 23:02:14 2006 +0100
@@ -25,12 +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: 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 cases_type: string -> attribute
+ val cases_set: string -> attribute
+ val induct_type: string -> attribute
+ val induct_set: string -> attribute
+ val coinduct_type: string -> attribute
+ val coinduct_set: string -> attribute
val casesN: string
val inductN: string
val coinductN: string
@@ -225,8 +225,8 @@
val _ = Context.add_setup
(Attrib.add_attributes
- [(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")]);
+ [(casesN, cases_att, "declaration of cases rule for type or set"),
+ (inductN, induct_att, "declaration of induction rule for type or set"),
+ (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
end;
--- a/src/Pure/Isar/isar_thy.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/isar_thy.ML Sat Jan 21 23:02:14 2006 +0100
@@ -8,16 +8,16 @@
signature ISAR_THY =
sig
val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
- val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory
val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
- val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
+ val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory
val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
- val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
+ val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
val theorems: string ->
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-> theory -> (string * thm list) list * theory
val theorems_i: string ->
- ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
+ ((bstring * attribute list) * (thm list * attribute list) list) list
-> theory -> (string * thm list) list * theory
val smart_theorems: string -> xstring option ->
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
@@ -34,7 +34,7 @@
bool -> Proof.state -> Proof.state
val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
theory -> Proof.state
- val theorem_i: string -> string * theory attribute list -> term * (term list * term list) ->
+ val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
theory -> Proof.state
val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
val terminal_proof: Method.text * Method.text option ->
@@ -58,7 +58,7 @@
(* axioms and defs *)
fun add_axms f args thy =
- f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
+ f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
val add_axioms = add_axms (snd oo PureThy.add_axioms);
val add_axioms_i = snd oo PureThy.add_axioms_i;
@@ -73,7 +73,7 @@
Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
fun theorems kind args thy = thy
- |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
+ |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.attribute thy) args)
|> tap (present_theorems kind);
fun theorems_i kind args =
--- a/src/Pure/Isar/locale.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/locale.ML Sat Jan 21 23:02:14 2006 +0100
@@ -72,7 +72,7 @@
(* Storing results *)
val smart_note_thmss: string -> string option ->
- ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
+ ((bstring * attribute list) * (thm list * attribute list) list) list ->
theory -> (bstring * thm list) list * theory
val note_thmss: string -> xstring ->
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
@@ -86,8 +86,8 @@
((string * Attrib.src list) * (string * (string list * string list)) list) list ->
theory -> Proof.state
val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
- string * theory attribute list -> Element.context_i element list ->
- ((string * theory attribute list) * (term * (term list * term list)) list) list ->
+ string * attribute list -> Element.context_i element list ->
+ ((string * attribute list) * (term * (term list * term list)) list) list ->
theory -> Proof.state
val theorem_in_locale: string -> Method.text option ->
(thm list list -> thm list list -> theory -> theory) ->
@@ -838,7 +838,7 @@
((ctxt, mode), [])
| activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
let
- val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
+ val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
val ts = List.concat (map (map #1 o #2) asms');
val (ps, qs) = splitAt (length ts, axs);
val (_, ctxt') =
@@ -849,7 +849,7 @@
((ctxt, Derived ths), [])
| activate_elem _ ((ctxt, Assumed axs), Defines defs) =
let
- val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
+ val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val (_, ctxt') =
ctxt |> ProofContext.add_assms_i ProofContext.def_export
(defs' |> map (fn ((name, atts), (t, ps)) =>
@@ -860,7 +860,7 @@
((ctxt, Derived ths), [])
| activate_elem is_ext ((ctxt, mode), Notes facts) =
let
- val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
+ val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
in ((ctxt', mode), if is_ext then res else []) end;
@@ -1445,7 +1445,7 @@
(Element.inst_term insts) (Element.inst_thm thy insts);
val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
((NameSpace.qualified prfx n,
- map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)),
+ map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
[(map (Drule.standard o satisfy_protected prems o
Element.inst_thm thy insts) ths, [])]));
in global_note_accesses_i (Drule.kind kind) prfx args' thy |> snd end;
@@ -1777,7 +1777,7 @@
in
-val theorem = gen_theorem Attrib.global_attribute intern_attrib read_context_statement;
+val theorem = gen_theorem Attrib.attribute intern_attrib read_context_statement;
val theorem_i = gen_theorem (K I) (K I) cert_context_statement;
val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib
@@ -1875,7 +1875,7 @@
(fn thy => fn (name, ps) =>
get_global_registration thy (name, map Logic.varify ps))
(swap ooo global_note_accesses_i (Drule.kind ""))
- Attrib.global_attribute_i Drule.standard
+ Attrib.attribute_i Drule.standard
(fn (name, ps) => put_global_registration (name, map Logic.varify ps))
(fn (n, ps) => fn (t, th) =>
add_global_witness (n, map Logic.varify ps)
@@ -1884,7 +1884,7 @@
fun local_activate_facts_elemss x = gen_activate_facts_elemss
get_local_registration
local_note_accesses_i
- Attrib.context_attribute_i I
+ (Attrib.attribute_i o ProofContext.theory_of) I
put_local_registration
add_local_witness x;
@@ -2067,11 +2067,11 @@
fun activate_elem (Notes facts) thy =
let
val facts' = facts
- |> Attrib.map_facts (Attrib.global_attribute_i thy o
+ |> Attrib.map_facts (Attrib.attribute_i thy o
Args.map_values I (Element.instT_type (#1 insts))
(Element.inst_term insts)
(disch o Element.inst_thm thy insts o satisfy))
- |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
+ |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
|> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
|> map (apfst (apfst (NameSpace.qualified prfx)))
in
--- a/src/Pure/Isar/method.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/method.ML Sat Jan 21 23:02:14 2006 +0100
@@ -581,7 +581,7 @@
val add_method = add_methods o Library.single;
-fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
+fun Method name meth cmt = Context.>> (add_method (name, meth, cmt));
(* method_setup *)
@@ -615,7 +615,7 @@
(* sections *)
-type modifier = (ProofContext.context -> ProofContext.context) * ProofContext.context attribute;
+type modifier = (ProofContext.context -> ProofContext.context) * attribute;
local
@@ -623,7 +623,7 @@
fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
fun thmss ss = Scan.repeat (thms ss) >> List.concat;
-fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
+fun apply (f, att) (ctxt, ths) = foldl_map (Thm.proof_attributes [att]) (f ctxt, ths);
fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
Scan.succeed (apply m (ctxt, ths)))) >> #2;
@@ -662,13 +662,13 @@
>> (pair (I: ProofContext.context -> ProofContext.context) o att);
val iprover_modifiers =
- [modifier destN Args.bang_colon Args.bang (Attrib.context o ContextRules.dest_bang),
- modifier destN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.dest),
- modifier elimN Args.bang_colon Args.bang (Attrib.context o ContextRules.elim_bang),
- modifier elimN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.elim),
- modifier introN Args.bang_colon Args.bang (Attrib.context o ContextRules.intro_bang),
- modifier introN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.intro),
- Args.del -- Args.colon >> K (I, Attrib.context ContextRules.rule_del)];
+ [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
+ modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
+ modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
+ modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
+ modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
+ modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
+ Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
in
--- a/src/Pure/Isar/object_logic.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Jan 21 23:02:14 2006 +0100
@@ -14,8 +14,8 @@
val drop_judgment: theory -> term -> term
val fixed_judgment: theory -> string -> term
val ensure_propT: theory -> term -> term
- val declare_atomize: theory attribute
- val declare_rulify: theory attribute
+ val declare_atomize: attribute
+ val declare_rulify: attribute
val atomize_term: theory -> term -> term
val atomize_cterm: theory -> cterm -> thm
val atomize_thm: thm -> thm
@@ -24,8 +24,8 @@
val atomize_goal: int -> thm -> thm
val rulify: thm -> thm
val rulify_no_asm: thm -> thm
- val rule_format: 'a attribute
- val rule_format_no_asm: 'a attribute
+ val rule_format: attribute
+ val rule_format_no_asm: attribute
end;
structure ObjectLogic: OBJECT_LOGIC =
@@ -123,11 +123,13 @@
val get_atomize = #1 o #2 o ObjectLogicData.get;
val get_rulify = #2 o #2 o ObjectLogicData.get;
-val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
-val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
+val declare_atomize =
+ Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
+ Library.apsnd o Library.apfst o Drule.add_rule);
-fun declare_atomize (thy, th) = (add_atomize th thy, th);
-fun declare_rulify (thy, th) = (add_rulify th thy, th);
+val declare_rulify =
+ Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o
+ Library.apsnd o Library.apsnd o Drule.add_rule);
(* atomize *)
@@ -164,8 +166,8 @@
val rulify = gen_rulify true;
val rulify_no_asm = gen_rulify false;
-fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
-fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
+fun rule_format x = Thm.rule_attribute (fn _ => rulify) x;
+fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x;
end;
--- a/src/Pure/Isar/obtain.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/obtain.ML Sat Jan 21 23:02:14 2006 +0100
@@ -40,7 +40,7 @@
((string * Attrib.src list) * (string * (string list * string list)) list) list
-> bool -> Proof.state -> Proof.state
val obtain_i: (string * typ option) list ->
- ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
+ ((string * attribute list) * (term * (term list * term list)) list) list
-> bool -> Proof.state -> Proof.state
val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
@@ -137,7 +137,7 @@
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(thesisN, NONE)]
|> Proof.assume_i
- [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
+ [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
@@ -146,7 +146,7 @@
in
-val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
+val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
end;
--- a/src/Pure/Isar/proof.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/proof.ML Sat Jan 21 23:02:14 2006 +0100
@@ -47,19 +47,19 @@
((string * Attrib.src list) * (string * (string list * string list)) list) list ->
state -> state
val assm_i: ProofContext.export ->
- ((string * context attribute list) * (term * (term list * term list)) list) list
+ ((string * attribute list) * (term * (term list * term list)) list) list
-> state -> state
val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
state -> state
- val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
+ val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
-> state -> state
val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
-> state -> state
- val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
+ val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
-> state -> state
val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
state -> state
- val def_i: ((string * context attribute list) * (string * (term * term list))) list ->
+ val def_i: ((string * attribute list) * (string * (term * term list))) list ->
state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
@@ -67,18 +67,18 @@
val simple_note_thms: string -> thm list -> state -> state
val note_thmss: ((string * Attrib.src list) *
(thmref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((string * context attribute list) *
- (thm list * context attribute list) list) list -> state -> state
+ val note_thmss_i: ((string * attribute list) *
+ (thm list * attribute list) list) list -> state -> state
val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
- val from_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+ val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
- val with_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+ val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
val using: ((thmref * Attrib.src list) list) list -> state -> state
- val using_i: ((thm list * context attribute list) list) list -> state -> state
+ val using_i: ((thm list * attribute list) list) list -> state -> state
val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
- val unfolding_i: ((thm list * context attribute list) list) list -> state -> state
+ val unfolding_i: ((thm list * attribute list) list) list -> state -> state
val invoke_case: string * string option list * Attrib.src list -> state -> state
- val invoke_case_i: string * string option list * context attribute list -> state -> state
+ val invoke_case_i: string * string option list * attribute list -> state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state Seq.seq
@@ -89,13 +89,13 @@
val apply_end: Method.text -> state -> state Seq.seq
val goal_names: string option -> string -> string list -> string
val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
- (theory -> 'a -> context attribute) ->
+ (theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
((string * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state Seq.seq
val global_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
- (theory -> 'a -> theory attribute) ->
+ (theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> theory -> theory) ->
string option -> string * 'a list -> ((string * 'a list) * 'b) list -> context -> state
@@ -114,21 +114,21 @@
((string * Attrib.src list) * (string * (string list * string list)) list) list ->
bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * context attribute list) * (term * (term list * term list)) list) list ->
+ ((string * attribute list) * (term * (term list * term list)) list) list ->
bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
((string * Attrib.src list) * (string * (string list * string list)) list) list ->
bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * context attribute list) * (term * (term list * term list)) list) list ->
+ ((string * attribute list) * (term * (term list * term list)) list) list ->
bool -> state -> state
val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
string option -> string * Attrib.src list ->
((string * Attrib.src list) * (string * (string list * string list)) list) list ->
context -> state
val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
- string option -> string * theory attribute list ->
- ((string * theory attribute list) * (term * (term list * term list)) list) list ->
+ string option -> string * attribute list ->
+ ((string * attribute list) * (term * (term list * term list)) list) list ->
context -> state
end;
@@ -534,7 +534,7 @@
in
-val assm = gen_assume ProofContext.add_assms Attrib.local_attribute;
+val assm = gen_assume ProofContext.add_assms Attrib.attribute;
val assm_i = gen_assume ProofContext.add_assms_i (K I);
val assume = assm ProofContext.assume_export;
val assume_i = assm_i ProofContext.assume_export;
@@ -566,7 +566,7 @@
in
-val def = gen_def fix Attrib.local_attribute ProofContext.match_bind;
+val def = gen_def fix Attrib.attribute ProofContext.match_bind;
val def_i = gen_def fix_i (K I) ProofContext.match_bind_i;
end;
@@ -603,15 +603,15 @@
in
-val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.local_attribute;
+val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.attribute;
val note_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) I #2 (K I);
val from_thmss =
- gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.local_attribute o no_binding;
+ gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.attribute o no_binding;
val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain #2 (K I) o no_binding;
val with_thmss =
- gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.local_attribute o no_binding;
+ gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.attribute o no_binding;
val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain #2 (K I) o no_binding;
val local_results = gen_thmss ProofContext.note_thmss_i (K []) I I (K I);
@@ -642,9 +642,9 @@
in
-val using = gen_using append_using (K I) ProofContext.note_thmss Attrib.local_attribute;
+val using = gen_using append_using (K I) ProofContext.note_thmss Attrib.attribute;
val using_i = gen_using append_using (K I) ProofContext.note_thmss_i (K I);
-val unfolding = gen_using unfold_using unfold_goal ProofContext.note_thmss Attrib.local_attribute;
+val unfolding = gen_using unfold_using unfold_goal ProofContext.note_thmss Attrib.attribute;
val unfolding_i = gen_using unfold_using unfold_goal ProofContext.note_thmss_i (K I);
end;
@@ -671,7 +671,7 @@
in
-val invoke_case = gen_invoke_case Attrib.local_attribute;
+val invoke_case = gen_invoke_case Attrib.attribute;
val invoke_case_i = gen_invoke_case (K I);
end;
@@ -957,11 +957,11 @@
in
-val have = gen_have Attrib.local_attribute ProofContext.bind_propp;
+val have = gen_have Attrib.attribute ProofContext.bind_propp;
val have_i = gen_have (K I) ProofContext.bind_propp_i;
-val show = gen_show Attrib.local_attribute ProofContext.bind_propp;
+val show = gen_show Attrib.attribute ProofContext.bind_propp;
val show_i = gen_show (K I) ProofContext.bind_propp_i;
-val theorem = gen_theorem Attrib.global_attribute ProofContext.bind_propp_schematic;
+val theorem = gen_theorem Attrib.attribute ProofContext.bind_propp_schematic;
val theorem_i = gen_theorem (K I) ProofContext.bind_propp_schematic_i;
end;
--- a/src/Pure/Isar/proof_context.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Jan 21 23:02:14 2006 +0100
@@ -109,10 +109,10 @@
val hide_thms: bool -> string list -> context -> context
val put_thms: string * thm list option -> context -> context
val note_thmss:
- ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
+ ((bstring * attribute list) * (thmref * attribute list) list) list ->
context -> (bstring * thm list) list * context
val note_thmss_i:
- ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
+ ((bstring * attribute list) * (thm list * attribute list) list) list ->
context -> (bstring * thm list) list * context
val read_vars: (string * string option * mixfix) list -> context ->
(string * typ option * mixfix) list * context
@@ -129,10 +129,10 @@
val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
val bind_fixes: string list -> context -> (term -> term) * context
val add_assms: export ->
- ((string * context attribute list) * (string * (string list * string list)) list) list ->
+ ((string * attribute list) * (string * (string list * string list)) list) list ->
context -> (bstring * thm list) list * context
val add_assms_i: export ->
- ((string * context attribute list) * (term * (term list * term list)) list) list ->
+ ((string * attribute list) * (term * (term list * term list)) list) list ->
context -> (bstring * thm list) list * context
val assume_export: export
val presume_export: export
@@ -1042,7 +1042,7 @@
fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
let
fun app (th, attrs) (ct, ths) =
- let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th)
+ let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th)
in (ct', th' :: ths) end;
val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
val thms = List.concat (rev rev_thms);
--- a/src/Pure/Isar/rule_cases.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sat Jan 21 23:02:14 2006 +0100
@@ -33,15 +33,15 @@
val consume: thm list -> thm list -> ('a * int) * thm ->
(('a * (int * thm list)) * thm) Seq.seq
val add_consumes: int -> thm -> thm
- val consumes: int -> 'a attribute
- val consumes_default: int -> 'a attribute
+ val consumes: int -> attribute
+ val consumes_default: int -> attribute
val name: string list -> thm -> thm
- val case_names: string list -> 'a attribute
- val case_conclusion: string * string list -> 'a attribute
+ val case_names: string list -> attribute
+ val case_conclusion: string * string list -> attribute
val save: thm -> thm -> thm
val get: thm -> (string * string list) list * int
val rename_params: string list list -> thm -> thm
- val params: string list list -> 'a attribute
+ val params: string list list -> attribute
val mutual_rule: thm list -> (int list * thm) option
val strict_mutual_rule: thm list -> int list * thm
end;
@@ -232,7 +232,7 @@
val save_consumes = put_consumes o lookup_consumes;
-fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
+fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
fun consumes_default n x =
if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
@@ -251,7 +251,7 @@
val save_case_names = add_case_names o lookup_case_names;
val name = add_case_names o SOME;
-fun case_names ss = Drule.rule_attribute (K (name ss));
+fun case_names ss = Thm.rule_attribute (K (name ss));
@@ -277,7 +277,7 @@
| _ => NONE)
in fold add_case_concl concls end;
-fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
+fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
@@ -304,7 +304,7 @@
|> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
|> save th;
-fun params xss = Drule.rule_attribute (K (rename_params xss));
+fun params xss = Thm.rule_attribute (K (rename_params xss));
--- a/src/Pure/Isar/specification.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/specification.ML Sat Jan 21 23:02:14 2006 +0100
@@ -13,18 +13,18 @@
(string * string option * mixfix) list *
((string * Attrib.src list) * string list) list -> Proof.context ->
((string * typ * mixfix) list *
- ((string * Context.generic attribute list) * term list) list) * Proof.context
+ ((string * attribute list) * term list) list) * Proof.context
val cert_specification:
(string * typ option * mixfix) list *
- ((string * Context.generic attribute list) * term list) list -> Proof.context ->
+ ((string * attribute list) * term list) list -> Proof.context ->
((string * typ * mixfix) list *
- ((string * Context.generic attribute list) * term list) list) * Proof.context
+ ((string * attribute list) * term list) list) * Proof.context
val axiomatize:
(string * string option * mixfix) list *
((bstring * Attrib.src list) * string list) list -> theory -> thm list list * theory
val axiomatize_i:
(string * typ option * mixfix) list *
- ((bstring * Context.generic attribute list) * term list) list -> theory ->
+ ((bstring * attribute list) * term list) list -> theory ->
thm list list * theory
end;
@@ -61,7 +61,7 @@
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
fun read_specification x =
- prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.generic_attribute x;
+ prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.attribute x;
fun cert_specification x =
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
@@ -73,7 +73,7 @@
val ((consts, specs), ctxt) = prep args (ProofContext.init thy);
val subst = consts |> map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T)));
val axioms = specs |> map (fn ((name, att), ts) =>
- ((name, map (Term.subst_atomic subst) ts), map Attrib.theory att));
+ ((name, map (Term.subst_atomic subst) ts), att));
val (thms, thy') =
thy
|> Theory.add_consts_i consts
--- a/src/Pure/Proof/extraction.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Jan 21 23:02:14 2006 +0100
@@ -355,7 +355,7 @@
(** expanding theorems / definitions **)
-fun add_expand_thm (thy, thm) =
+fun add_expand_thm thm thy =
let
val {realizes_eqns, typeof_eqns, types, realizers,
defs, expand, prep} = ExtractionData.get thy;
@@ -379,10 +379,13 @@
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = (name, prop_of thm) ins expand, prep = prep}) thy, thm)
+ expand = (name, prop_of thm) ins expand, prep = prep}) thy)
end;
-fun add_expand_thms thms thy = Library.foldl (fst o add_expand_thm) (thy, thms);
+val add_expand_thms = fold add_expand_thm;
+
+val extraction_expand =
+ Attrib.no_args (Thm.declaration_attribute (Context.map_theory o add_expand_thm));
(** types with computational content **)
@@ -445,8 +448,7 @@
\ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
Attrib.add_attributes
- [("extraction_expand",
- (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
+ [("extraction_expand", extraction_expand,
"specify theorems / definitions to be expanded during extraction")]);
--- a/src/Pure/Tools/class_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -15,7 +15,7 @@
-> ((bstring * string) * Attrib.src list) list
-> theory -> Proof.state
val add_instance_arity_i: (string * sort list) * sort
- -> ((bstring * term) * theory attribute list) list
+ -> ((bstring * term) * attribute list) list
-> theory -> Proof.state
val add_classentry: class -> xstring list -> xstring list -> theory -> theory
--- a/src/Pure/axclass.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/axclass.ML Sat Jan 21 23:02:14 2006 +0100
@@ -12,7 +12,7 @@
val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
theory -> {intro: thm, axioms: thm list} * theory
- val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
+ val add_axclass_i: bstring * class list -> ((bstring * term) * attribute list) list ->
theory -> {intro: thm, axioms: thm list} * theory
val add_classrel_thms: thm list -> theory -> theory
val add_arity_thms: thm list -> theory -> theory
@@ -216,7 +216,7 @@
in
-val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
+val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.attribute;
val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
end;
--- a/src/Pure/codegen.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/codegen.ML Sat Jan 21 23:02:14 2006 +0100
@@ -26,7 +26,7 @@
val add_codegen: string -> term codegen -> theory -> theory
val add_tycodegen: string -> typ codegen -> theory -> theory
- val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
+ val add_attribute: string -> (Args.T list -> attribute * Args.T list) -> theory -> theory
val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
val preprocess: theory -> thm list -> thm list
val preprocess_term: theory -> term -> term
@@ -207,7 +207,7 @@
tycodegens : (string * typ codegen) list,
consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
types : (string * (typ mixfix list * (string * string) list)) list,
- attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
+ attrs: (string * (Args.T list -> attribute * Args.T list)) list,
preprocs: (stamp * (theory -> thm list -> thm list)) list,
modules: codegr Symtab.table,
test_params: test_params};
@@ -312,13 +312,11 @@
fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
val code_attr =
- Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
- (#attrs (CodegenData.get thy)))));
+ Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
+ (#attrs (CodegenData.get (Context.theory_of context))))));
val _ = Context.add_setup
- (Attrib.add_attributes
- [("code", (code_attr, K Attrib.undef_local_attribute),
- "declare theorems for code generation")]);
+ (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
(**** preprocessors ****)
@@ -348,10 +346,9 @@
| _ => err ()
end;
-fun unfold_attr (thy, eqn) =
+val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory
let
- val names = term_consts
- (fst (Logic.dest_equals (prop_of eqn)));
+ val names = term_consts (fst (Logic.dest_equals (prop_of eqn)));
fun prep thy = map (fn th =>
let val prop = prop_of th
in
@@ -359,7 +356,7 @@
then rewrite_rule [eqn] (Thm.transfer thy th)
else th
end)
- in (add_preprocessor prep thy, eqn) end;
+ in add_preprocessor prep end);
val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
--- a/src/Pure/pure_thy.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/pure_thy.ML Sat Jan 21 23:02:14 2006 +0100
@@ -47,35 +47,30 @@
val thms_of: theory -> (string * thm) list
val all_thms_of: theory -> (string * thm) list
val hide_thms: bool -> string list -> theory -> theory
- val store_thm: (bstring * thm) * theory attribute list -> theory -> thm * theory
+ val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
val smart_store_thms: (bstring * thm list) -> thm list
val smart_store_thms_open: (bstring * thm list) -> thm list
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
- val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> thm list * theory
- val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
- -> thm list list * theory
- val note_thmss: theory attribute -> ((bstring * theory attribute list) *
- (thmref * theory attribute list) list) list ->
- theory -> (bstring * thm list) list * theory
- val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
- (thm list * theory attribute list) list) list ->
- theory -> (bstring * thm list) list * theory
- val add_axioms: ((bstring * string) * theory attribute list) list ->
+ val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
+ val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
+ val note_thmss: attribute -> ((bstring * attribute list) *
+ (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+ val note_thmss_i: attribute -> ((bstring * attribute list) *
+ (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+ val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
+ val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
+ val add_axiomss: ((bstring * string list) * attribute list) list ->
+ theory -> thm list list * theory
+ val add_axiomss_i: ((bstring * term list) * attribute list) list ->
+ theory -> thm list list * theory
+ val add_defs: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
- val add_axioms_i: ((bstring * term) * theory attribute list) list ->
+ val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
theory -> thm list * theory
- val add_axiomss: ((bstring * string list) * theory attribute list) list ->
- theory -> thm list list * theory
- val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
+ val add_defss: bool -> ((bstring * string list) * attribute list) list ->
theory -> thm list list * theory
- val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
- theory -> thm list * theory
- val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
- theory -> thm list * theory
- val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
- theory -> thm list list * theory
- val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
+ val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
theory -> thm list list * theory
val generic_setup: string option -> theory -> theory
val add_oracle: bstring * string * string -> theory -> theory
@@ -340,8 +335,7 @@
(* add_thms(s) *)
fun add_thms_atts pre_name ((bname, thms), atts) =
- enter_thms pre_name (name_thms false)
- (Thm.applys_attributes atts) (bname, thms);
+ enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -359,7 +353,7 @@
fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
let
- fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
+ fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
val (thms, thy') = thy |> enter_thms
name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
(bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
--- a/src/Pure/simplifier.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/simplifier.ML Sat Jan 21 23:02:14 2006 +0100
@@ -64,11 +64,11 @@
val print_local_simpset: Proof.context -> unit
val get_local_simpset: Proof.context -> simpset
val put_local_simpset: simpset -> Proof.context -> Proof.context
- val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
- val simp_add: Context.generic attribute
- val simp_del: Context.generic attribute
- val cong_add: Context.generic attribute
- val cong_del: Context.generic attribute
+ val attrib: (simpset * thm list -> simpset) -> attribute
+ val simp_add: attribute
+ val simp_del: attribute
+ val cong_add: attribute
+ val cong_del: attribute
val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
@@ -138,7 +138,7 @@
(* attributes *)
-fun attrib f = Attrib.declaration (fn th =>
+fun attrib f = Thm.declaration_attribute (fn th =>
fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
| Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
@@ -251,7 +251,7 @@
in
val simplified =
- Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
+ Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
end;
@@ -261,11 +261,9 @@
val _ = Context.add_setup
(Attrib.add_attributes
- [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
- "declaration of Simplifier rule"),
- (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
- "declaration of Simplifier congruence rule"),
- ("simplified", Attrib.common simplified, "simplified rule")]);
+ [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"),
+ (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
+ ("simplified", simplified, "simplified rule")]);
@@ -286,23 +284,23 @@
>> (curry (Library.foldl op o) I o rev)) x;
val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
- Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
- Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
+ [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
+ Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
+ Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
- Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
- Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+ [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
+ Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
+ Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
- >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
+ >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
@ cong_modifiers;
val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+ [Args.add -- Args.colon >> K (I, simp_add),
+ Args.del -- Args.colon >> K (I, simp_del),
Args.$$$ onlyN -- Args.colon
- >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
+ >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
@ cong_modifiers;
fun simp_args more_mods =
--- a/src/ZF/Tools/datatype_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -367,8 +367,8 @@
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
|> PureThy.add_thmss
- [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
- (("", intrs), [Attrib.theory (Classical.safe_intro NONE)]),
+ [(("simps", simps), [Simplifier.simp_add]),
+ (("", intrs), [Classical.safe_intro NONE]),
(("con_defs", con_defs), []),
(("case_eqns", case_eqns), []),
(("recursor_eqns", recursor_eqns), []),
--- a/src/ZF/Tools/ind_cases.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML Sat Jan 21 23:02:14 2006 +0100
@@ -53,7 +53,7 @@
val read_prop = ProofContext.read_prop (ProofContext.init thy);
val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
val facts = args |> map (fn ((name, srcs), props) =>
- ((name, map (Attrib.global_attribute thy) srcs),
+ ((name, map (Attrib.attribute thy) srcs),
map (Thm.no_attributes o single o mk_cases) props));
in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
--- a/src/ZF/Tools/induct_tacs.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sat Jan 21 23:02:14 2006 +0100
@@ -165,7 +165,7 @@
in
thy
|> Theory.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
+ |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Theory.parent_path
--- a/src/ZF/Tools/inductive_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -29,7 +29,7 @@
(*Insert definitions for the recursive sets, which
must *already* be declared as constants in parent theory!*)
val add_inductive_i: bool -> term list * term ->
- ((bstring * term) * theory attribute list) list ->
+ ((bstring * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
((bstring * string) * Attrib.src list) list ->
@@ -515,7 +515,7 @@
val ([induct', mutual_induct'], thy') =
thy
|> PureThy.add_thms [((co_prefix ^ "induct", induct),
- [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]),
+ [case_names, InductAttrib.induct_set big_rec_name]),
(("mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -537,7 +537,7 @@
|> PureThy.add_thms
[(("bnd_mono", bnd_mono), []),
(("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])]
+ (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];
@@ -561,7 +561,7 @@
fun add_inductive (srec_tms, sdom_sum) intr_srcs
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
- val intr_atts = map (map (Attrib.global_attribute thy) o snd) intr_srcs;
+ val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
val sintrs = map fst intr_srcs ~~ intr_atts;
val read = Sign.simple_read_term thy;
val rec_tms = map (read Ind_Syntax.iT) srec_tms;
--- a/src/ZF/Tools/primrec_package.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML Sat Jan 21 23:02:14 2006 +0100
@@ -11,7 +11,7 @@
sig
val quiet_mode: bool ref
val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
- val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
+ val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -191,13 +191,13 @@
|> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
- |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])]
+ |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
||> Theory.parent_path;
in (thy3, eqn_thms') end;
fun add_primrec args thy =
add_primrec_i (map (fn ((name, s), srcs) =>
- ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs))
+ ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.attribute thy) srcs))
args) thy;