src/Pure/Isar/new_locale.ML
changeset 29018 17538bdef546
parent 28994 49f602ae24e5
child 29019 8e7d6f959bd7
     1.1 --- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 16:41:36 2008 +0100
     1.3 @@ -37,10 +37,8 @@
     1.4    (* Activation *)
     1.5    val activate_declarations: theory -> string * Morphism.morphism ->
     1.6      Proof.context -> Proof.context
     1.7 -  val activate_global_facts: string * Morphism.morphism ->
     1.8 -    theory -> theory
     1.9 -  val activate_local_facts: theory -> string * Morphism.morphism ->
    1.10 -    Proof.context -> Proof.context
    1.11 +  val activate_global_facts: string * Morphism.morphism -> theory -> theory
    1.12 +  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
    1.13  (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
    1.14    val init: string -> theory -> Proof.context
    1.15  
    1.16 @@ -360,8 +358,9 @@
    1.17    roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
    1.18    uncurry put_global_idents;
    1.19  
    1.20 -fun activate_local_facts thy dep ctxt =
    1.21 -  roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |>
    1.22 +fun activate_local_facts dep ctxt =
    1.23 +  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
    1.24 +    (get_local_idents ctxt, ctxt) |>
    1.25    uncurry put_local_idents;
    1.26  
    1.27  fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
    1.28 @@ -454,8 +453,9 @@
    1.29        "back-chain all introduction rules of locales")]));
    1.30  
    1.31  
    1.32 -(*** Registrations: interpretations in theories and proof contexts ***)
    1.33 +(*** Registrations: interpretations in theories ***)
    1.34  
    1.35 +(* FIXME only global variant needed *)
    1.36  structure RegistrationsData = GenericDataFun
    1.37  (
    1.38    type T = ((string * Morphism.morphism) * stamp) list;
    1.39 @@ -470,6 +470,5 @@
    1.40  fun add_global_registration reg =
    1.41    (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
    1.42  
    1.43 -
    1.44  end;
    1.45