partial evaluation of locale facts leads to static scoping of rule attributes;

--- a/src/Pure/Isar/named_target.ML	Fri Nov 18 21:50:50 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Fri Nov 18 21:55:24 2011 +0100
@@ -118,8 +118,9 @@
 fun locale_notes locale kind global_facts local_facts lthy =
   let
     val global_facts' = Attrib.map_facts (K []) global_facts;
-    val local_facts' = Element.facts_map
-      (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
+    val local_facts' = local_facts
+      |> Attrib.partial_evaluation lthy
+      |> Element.facts_map (Element.transform_ctxt (Local_Theory.target_morphism lthy));
   in
     lthy
     |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)