# HG changeset patch # User wenzelm # Date 1137880934 -3600 # Node ID 6790126ab5f6d308d5fb6bbb7f29aef7fcf63443 # Parent caf9bc780c8086d91fd8fa58861f3ead627641d6 simplified type attribute; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Import/hol4rews.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Import/proof_kernel.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Import/shuffler.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/datatype_abs_proofs.ML --- 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 -> diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/datatype_aux.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/datatype_package.ML --- 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 |> diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/datatype_rep_proofs.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/inductive_package.ML --- 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 *) diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/inductive_realizer.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/primrec_package.ML --- 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))) diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/recdef_package.ML --- 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 *) diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/recfun_codegen.ML --- 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') = diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/record_package.ML --- 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' diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/res_axioms.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/split_rule.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/typedef_package.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/arith_data.ML --- 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")]; diff -r caf9bc780c80 -r 6790126ab5f6 src/HOLCF/domain/theorems.ML --- 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 *) diff -r caf9bc780c80 -r 6790126ab5f6 src/HOLCF/fixrec_package.ML --- 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); diff -r caf9bc780c80 -r 6790126ab5f6 src/HOLCF/pcpodef_package.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/Provers/clasimp.ML --- 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"), diff -r caf9bc780c80 -r 6790126ab5f6 src/Provers/classical.ML --- 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)); diff -r caf9bc780c80 -r 6790126ab5f6 src/Provers/splitter.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/args.ML --- 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 | diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/calculation.ML --- 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); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/constdefs.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/context_rules.ML --- 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); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/induct_attrib.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/isar_thy.ML --- 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 = diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/locale.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/method.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/object_logic.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/obtain.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/proof.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/proof_context.ML --- 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); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/rule_cases.ML --- 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)); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Isar/specification.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Proof/extraction.ML --- 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")]); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/Tools/class_package.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/axclass.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/codegen.ML --- 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)); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/pure_thy.ML --- 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); diff -r caf9bc780c80 -r 6790126ab5f6 src/Pure/simplifier.ML --- 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 = diff -r caf9bc780c80 -r 6790126ab5f6 src/ZF/Tools/datatype_package.ML --- 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), []), diff -r caf9bc780c80 -r 6790126ab5f6 src/ZF/Tools/ind_cases.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/ZF/Tools/induct_tacs.ML --- 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 diff -r caf9bc780c80 -r 6790126ab5f6 src/ZF/Tools/inductive_package.ML --- 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; diff -r caf9bc780c80 -r 6790126ab5f6 src/ZF/Tools/primrec_package.ML --- 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;