# HG changeset patch
# User ballarin
# Date 1281471983 -7200
# Node ID 88e774d09fbcf98a059d25716ed934dc430e40b6
# Parent  fa3f90cf6d9c85bc5c0718108fb95103aea0a483
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.

diff -r fa3f90cf6d9c -r 88e774d09fbc src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Aug 10 15:09:39 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -451,7 +451,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       fix_params fixed |>
-      fold Locale.activate_declarations deps;
+      fold (Context.proof_map o Locale.activate_facts NONE) deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
       fold_map activate elems;
diff -r fa3f90cf6d9c -r 88e774d09fbc src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 10 15:09:39 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -53,7 +53,7 @@
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
-  val activate_facts: morphism -> string * morphism -> Context.generic -> Context.generic
+  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
@@ -422,8 +422,12 @@
 fun activate_facts export dep context =
   let
     val thy = Context.theory_of context;
-    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context (SOME export);
-  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
+    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
+  in
+    roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
+      dep (get_idents context, context)
+    |-> put_idents
+  end;
 
 fun init name thy =
   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
@@ -468,7 +472,7 @@
       |> (case mixin of NONE => I
            | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
-      |> activate_facts export (name, morph)
+      |> activate_facts (SOME export) (name, morph)
   end;