--- a/src/HOL/Tools/choice_specification.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Apr 27 22:47:30 2012 +0200
@@ -202,7 +202,7 @@
|> apfst undo_imps
|> apfst Drule.export_without_context
|-> Thm.theory_attributes
- (map (Attrib.attribute thy)
+ (map (Attrib.attribute_cmd_global thy)
(@{attributes [nitpick_choice_spec]} @ atts))
|> add_final
|> swap
--- a/src/HOL/Tools/recdef.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/HOL/Tools/recdef.ML Fri Apr 27 22:47:30 2012 +0200
@@ -220,7 +220,7 @@
|> Sign.parent_path;
in (thy, result) end;
-val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
+val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global 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 ();
--- a/src/Pure/Isar/attrib.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Apr 27 22:47:30 2012 +0200
@@ -15,8 +15,10 @@
val intern_src: theory -> src -> src
val pretty_attribs: Proof.context -> src list -> Pretty.T list
val defined: theory -> string -> bool
- val attribute: theory -> src -> attribute
- val attribute_i: theory -> src -> attribute
+ val attribute: Proof.context -> src -> attribute
+ val attribute_global: theory -> src -> attribute
+ val attribute_cmd: Proof.context -> src -> attribute
+ val attribute_cmd_global: theory -> src -> attribute
val map_specs: ('a list -> 'att list) ->
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a list -> 'att list) ->
@@ -120,7 +122,7 @@
val defined = Symtab.defined o #2 o Attributes.get;
-fun attribute_i thy =
+fun attribute_global thy =
let
val (space, tab) = Attributes.get thy;
fun attr src =
@@ -131,7 +133,11 @@
end;
in attr end;
-fun attribute thy = attribute_i thy o intern_src thy;
+val attribute = attribute_global o Proof_Context.theory_of;
+val attribute_generic = attribute_global o Context.theory_of;
+
+fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
+val attribute_cmd = attribute_cmd_global o Proof_Context.theory_of;
(* attributed declarations *)
@@ -145,17 +151,17 @@
(* fact expressions *)
fun global_notes kind facts thy = thy |>
- Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+ Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
fun local_notes kind facts ctxt = ctxt |>
- Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+ Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts);
fun generic_notes kind facts context = context |>
Context.mapping_result (global_notes kind facts) (local_notes kind facts);
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
- (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
+ (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
[((Binding.empty, []), srcs)])
|> fst |> maps snd;
@@ -203,7 +209,7 @@
in
Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
let
- val atts = map (attribute_i thy) srcs;
+ val atts = map (attribute_generic context) srcs;
val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
in (context', pick "" [th']) end)
||
@@ -215,7 +221,7 @@
-- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
let
val ths = Facts.select thmref fact;
- val atts = map (attribute_i thy) srcs;
+ val atts = map (attribute_generic context) srcs;
val (ths', context') =
fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
in (context', pick name ths') end)
@@ -240,7 +246,7 @@
fun apply_att src (context, th) =
let
val src1 = Args.assignable src;
- val result = attribute_i (Context.theory_of context) src1 (context, th);
+ val result = attribute_generic context src1 (context, th);
val src2 = Args.closure src1;
in (src2, result) end;
--- a/src/Pure/Isar/element.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/Isar/element.ML Fri Apr 27 22:47:30 2012 +0200
@@ -485,16 +485,14 @@
| init (Constrains _) = I
| init (Assumes asms) = Context.map_proof (fn ctxt =>
let
- val asms' =
- Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms;
+ val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
|> Proof_Context.add_assms_i Assumption.assume_export asms';
in ctxt' end)
| init (Defines defs) = Context.map_proof (fn ctxt =>
let
- val defs' =
- Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs;
+ val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
--- a/src/Pure/Isar/isar_cmd.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Apr 27 22:47:30 2012 +0200
@@ -192,7 +192,8 @@
fun add_defs ((unchecked, overloaded), args) thy =
thy |>
(if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
- overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
+ overloaded
+ (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
|> snd;
--- a/src/Pure/Isar/obtain.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Apr 27 22:47:30 2012 +0200
@@ -126,7 +126,7 @@
val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
val asm_props = maps (map fst) proppss;
- val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
+ val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
(*obtain parms*)
val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
@@ -168,7 +168,7 @@
in
val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
+val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.read_propp;
end;
--- a/src/Pure/Isar/proof.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/Isar/proof.ML Fri Apr 27 22:47:30 2012 +0200
@@ -83,7 +83,7 @@
val apply: Method.text -> state -> state Seq.seq
val apply_end: Method.text -> state -> state Seq.seq
val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
- (theory -> 'a -> attribute) ->
+ (Proof.context -> 'a -> attribute) ->
('b list -> context -> (term list list * (context -> context)) * context) ->
string -> Method.text option -> (thm list list -> state -> state) ->
((binding * 'a list) * 'b) list -> state -> state
@@ -400,7 +400,8 @@
fun no_goal_cases st = map (rpair NONE) (goals st);
fun goal_cases st =
- Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
+ Rule_Cases.make_common
+ (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
fun apply_method current_context meth state =
let
@@ -612,13 +613,13 @@
fun gen_assume asm prep_att exp args state =
state
|> assert_forward
- |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (theory_of state))) args))
+ |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
|> these_factss [] |> #2;
in
val assm = gen_assume Proof_Context.add_assms_i (K I);
-val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute;
+val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
val assume = assm Assumption.assume_export;
val assume_cmd = assm_cmd Assumption.assume_export;
val presume = assm Assumption.presume_export;
@@ -634,10 +635,8 @@
fun gen_def prep_att prep_vars prep_binds args state =
let
val _ = assert_forward state;
- val thy = theory_of state;
-
val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
- val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
+ val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
in
state
|> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
@@ -651,7 +650,7 @@
in
val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
-val def_cmd = gen_def Attrib.attribute Proof_Context.read_vars Proof_Context.match_bind;
+val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
end;
@@ -683,10 +682,8 @@
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
state
|> assert_forward
- |> map_context_result (Proof_Context.note_thmss ""
- (Attrib.map_facts_refs
- (map (prep_atts (theory_of state)))
- (prep_fact (context_of state)) args))
+ |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+ (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
|> these_factss (more_facts state)
||> opt_chain
|> opt_result;
@@ -694,13 +691,15 @@
in
val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
-val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute Proof_Context.get_fact;
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
-val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
+val from_thmss_cmd =
+ gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
-val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute Proof_Context.get_fact o no_binding;
+val with_thmss_cmd =
+ gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
@@ -715,9 +714,8 @@
state
|> assert_backward
|> map_context_result
- (Proof_Context.note_thmss ""
- (Attrib.map_facts_refs (map (prep_att (theory_of state))) (prep_fact (context_of state))
- (no_binding args)))
+ (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+ (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
|> (fn (named_facts, state') =>
state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
let
@@ -732,9 +730,9 @@
in
val using = gen_using append_using (K (K I)) (K I) (K I);
-val using_cmd = gen_using append_using (K (K I)) Attrib.attribute Proof_Context.get_fact;
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
-val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute Proof_Context.get_fact;
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
end;
@@ -748,7 +746,7 @@
fun gen_invoke_case prep_att (name, xs, raw_atts) state =
let
- val atts = map (prep_att (theory_of state)) raw_atts;
+ val atts = map (prep_att (context_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
@@ -762,7 +760,7 @@
in
val invoke_case = gen_invoke_case (K I);
-val invoke_case_cmd = gen_invoke_case Attrib.attribute;
+val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
end;
@@ -935,9 +933,8 @@
fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
let
- val thy = theory_of state;
val ((names, attss), propp) =
- Attrib.map_specs (map (prep_att thy)) stmt |> split_list |>> split_list;
+ Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
fun after_qed' results =
local_results ((names ~~ attss) ~~ results)
@@ -1044,9 +1041,9 @@
in
val have = gen_have (K I) Proof_Context.bind_propp_i;
-val have_cmd = gen_have Attrib.attribute Proof_Context.bind_propp;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
val show = gen_show (K I) Proof_Context.bind_propp_i;
-val show_cmd = gen_show Attrib.attribute Proof_Context.bind_propp;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
end;
--- a/src/Pure/ML/ml_antiquote.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Apr 27 22:47:30 2012 +0200
@@ -88,8 +88,7 @@
macro (Binding.name "note")
(Args.context :|-- (fn ctxt =>
Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
- >> (fn ((a, srcs), ths) =>
- ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
+ >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
>> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
value (Binding.name "ctyp") (Args.typ >> (fn T =>
--- a/src/Pure/ML/ml_thms.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/Pure/ML/ml_thms.ML Fri Apr 27 22:47:30 2012 +0200
@@ -42,7 +42,7 @@
val i = serial ();
val srcs = map (Attrib.intern_src thy) raw_srcs;
- val _ = map (Attrib.attribute_i thy) srcs;
+ val _ = map (Attrib.attribute background) srcs;
val (a, background') = background
|> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
val ml =
--- a/src/ZF/Tools/ind_cases.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/ZF/Tools/ind_cases.ML Fri Apr 27 22:47:30 2012 +0200
@@ -48,7 +48,7 @@
let
val ctxt = Proof_Context.init_global thy;
val facts = args |> map (fn ((name, srcs), props) =>
- ((name, map (Attrib.attribute thy) srcs),
+ ((name, map (Attrib.attribute_cmd_global thy) srcs),
map (Thm.no_attributes o single o smart_cases ctxt) props));
in thy |> Global_Theory.note_thmss "" facts |> snd end;
--- a/src/ZF/Tools/inductive_package.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Apr 27 22:47:30 2012 +0200
@@ -558,7 +558,7 @@
val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
#> Syntax.check_terms ctxt;
- val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
+ val intr_atts = map (map (Attrib.attribute_cmd_global thy) o snd) intr_srcs;
val sintrs = map fst intr_srcs ~~ intr_atts;
val rec_tms = read_terms srec_tms;
val dom_sum = singleton read_terms sdom_sum;
--- a/src/ZF/Tools/primrec_package.ML Fri Apr 27 21:47:47 2012 +0200
+++ b/src/ZF/Tools/primrec_package.ML Fri Apr 27 22:47:30 2012 +0200
@@ -189,7 +189,7 @@
fun add_primrec args thy =
add_primrec_i (map (fn ((name, s), srcs) =>
- ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs))
+ ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs))
args) thy;