clarified signature;
authorwenzelm
Thu Aug 30 14:10:39 2018 +0200 (13 months ago)
changeset 68852becaeaa334ae
parent 68851 6c9825c1e26b
child 68853 d36f00510e40
clarified signature;
src/Pure/Isar/generic_target.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 13:38:52 2018 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:10:39 2018 +0200
     1.3 @@ -406,7 +406,7 @@
     1.4  
     1.5  fun locale_dependency locale registration =
     1.6    Local_Theory.raw_theory (Locale.add_dependency locale registration)
     1.7 -  #> Locale.activate_fragment_nonbrittle registration;
     1.8 +  #> Locale.add_registration_local_theory registration;
     1.9  
    1.10  
    1.11  (** locale abbreviations **)
     2.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 13:38:52 2018 +0200
     2.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:10:39 2018 +0200
     2.3 @@ -153,16 +153,11 @@
     2.4      (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     2.5      "interpret" propss eqns goal_ctxt state;
     2.6  
     2.7 -fun add_registration registration ctxt = ctxt
     2.8 -  |> Proof_Context.set_stmt false
     2.9 -  |> Context.proof_map (Locale.add_registration registration)
    2.10 -  |> Proof_Context.restore_stmt ctxt;
    2.11 -
    2.12  fun gen_interpret prep_interpretation expression state =
    2.13    Proof.assert_forward_or_chain state
    2.14    |> Proof.context_of
    2.15    |> generic_interpretation prep_interpretation (setup_proof state)
    2.16 -    Attrib.local_notes add_registration expression [];
    2.17 +    Attrib.local_notes Locale.add_registration_proof expression [];
    2.18  
    2.19  in
    2.20  
     3.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 13:38:52 2018 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:10:39 2018 +0200
     3.3 @@ -76,8 +76,9 @@
     3.4    type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
     3.5    val amend_registration: registration -> Context.generic -> Context.generic
     3.6    val add_registration: registration -> Context.generic -> Context.generic
     3.7 +  val add_registration_proof: registration -> Proof.context -> Proof.context
     3.8 +  val add_registration_local_theory: registration -> local_theory -> local_theory
     3.9    val activate_fragment: registration -> local_theory -> local_theory
    3.10 -  val activate_fragment_nonbrittle: registration -> local_theory -> local_theory
    3.11    val registrations_of: Context.generic -> string -> (string * morphism) list
    3.12    val add_dependency: string -> registration -> theory -> theory
    3.13  
    3.14 @@ -558,17 +559,23 @@
    3.15        |> activate_facts (SOME export) (name, morph)
    3.16    end;
    3.17  
    3.18 +fun add_registration_proof registration ctxt = ctxt
    3.19 +  |> Proof_Context.set_stmt false
    3.20 +  |> Context.proof_map (add_registration registration)
    3.21 +  |> Proof_Context.restore_stmt ctxt;
    3.22  
    3.23 -(* locale fragments within local theory *)
    3.24  
    3.25 -fun activate_fragment_nonbrittle registration lthy =
    3.26 +fun add_registration_local_theory registration lthy =
    3.27    let val n = Local_Theory.level lthy in
    3.28      lthy |> Local_Theory.map_contexts (fn level =>
    3.29        level = n - 1 ? Context.proof_map (add_registration registration))
    3.30    end;
    3.31  
    3.32 +
    3.33 +(* locale fragments within local theory *)
    3.34 +
    3.35  fun activate_fragment registration =
    3.36 -  Local_Theory.mark_brittle #> activate_fragment_nonbrittle registration;
    3.37 +  Local_Theory.mark_brittle #> add_registration_local_theory registration;
    3.38  
    3.39  
    3.40