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;