Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
authorballarin
Tue Aug 10 22:26:23 2010 +0200 (2010-08-10)
changeset 3831688e774d09fbc
parent 38315 fa3f90cf6d9c
child 38317 cb8e2ac6397b
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     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;
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 10 15:09:39 2010 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Aug 10 22:26:23 2010 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4  
     2.5    (* Activation *)
     2.6    val activate_declarations: string * morphism -> Proof.context -> Proof.context
     2.7 -  val activate_facts: morphism -> string * morphism -> Context.generic -> Context.generic
     2.8 +  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
     2.9    val init: string -> theory -> Proof.context
    2.10  
    2.11    (* Reasoning about locales *)
    2.12 @@ -422,8 +422,12 @@
    2.13  fun activate_facts export dep context =
    2.14    let
    2.15      val thy = Context.theory_of context;
    2.16 -    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context (SOME export);
    2.17 -  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
    2.18 +    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
    2.19 +  in
    2.20 +    roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
    2.21 +      dep (get_idents context, context)
    2.22 +    |-> put_idents
    2.23 +  end;
    2.24  
    2.25  fun init name thy =
    2.26    activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    2.27 @@ -468,7 +472,7 @@
    2.28        |> (case mixin of NONE => I
    2.29             | SOME mixin => amend_registration (name, morph) mixin export)
    2.30        (* activate import hierarchy as far as not already active *)
    2.31 -      |> activate_facts export (name, morph)
    2.32 +      |> activate_facts (SOME export) (name, morph)
    2.33    end;
    2.34  
    2.35