# HG changeset patch
# User wenzelm
# Date 1335559650 -7200
# Node ID 43f677b3ae91ff2126f936c83ab2a8704e708026
# Parent  53668571d300943a91879ac8a3874de534c1d47e
clarified signature;

diff -r 53668571d300 -r 43f677b3ae91 src/HOL/Tools/choice_specification.ML
--- 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
diff -r 53668571d300 -r 43f677b3ae91 src/HOL/Tools/recdef.ML
--- 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 ();
 
 
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/Isar/attrib.ML
--- 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;
 
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/Isar/element.ML
--- 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);
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/Isar/isar_cmd.ML
--- 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;
 
 
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/Isar/obtain.ML
--- 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;
 
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/Isar/proof.ML
--- 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;
 
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/ML/ml_antiquote.ML
--- 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 =>
diff -r 53668571d300 -r 43f677b3ae91 src/Pure/ML/ml_thms.ML
--- 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 =
diff -r 53668571d300 -r 43f677b3ae91 src/ZF/Tools/ind_cases.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;
 
diff -r 53668571d300 -r 43f677b3ae91 src/ZF/Tools/inductive_package.ML
--- 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;
diff -r 53668571d300 -r 43f677b3ae91 src/ZF/Tools/primrec_package.ML
--- 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;