src/Pure/Isar/expression.ML
changeset 38316 88e774d09fbc
parent 38211 8ed3a5fb4d25
child 38350 480b2de9927c
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Aug 10 15:09:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Aug 10 22:26:23 2010 +0200
     1.3 @@ -451,7 +451,7 @@
     1.4      (* Declare parameters and imported facts *)
     1.5      val context' = context |>
     1.6        fix_params fixed |>
     1.7 -      fold Locale.activate_declarations deps;
     1.8 +      fold (Context.proof_map o Locale.activate_facts NONE) deps;
     1.9      val (elems', _) = context' |>
    1.10        ProofContext.set_stmt true |>
    1.11        fold_map activate elems;