# HG changeset patch
# User wenzelm
# Date 1321649724 -3600
# Node ID ac32737ff69efcb00965a702bbfe1dd637aa45fb
# Parent  136e3faf74daf37754f7b846f40d79a05a61f244
partial evaluation of locale facts leads to static scoping of rule attributes;

diff -r 136e3faf74da -r ac32737ff69e src/Pure/Isar/named_target.ML
--- 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)