diff -r 7f4755c5e77b -r 8ed3a5fb4d25 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Aug 05 21:56:22 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 05 22:29:43 2010 +0200
@@ -451,7 +451,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       fix_params fixed |>
-      fold (Context.proof_map o Locale.activate_facts) deps;
+      fold Locale.activate_declarations deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
       fold_map activate elems;