tuned signature;
authorwenzelm
Thu Aug 30 14:21:40 2018 +0200 (13 months ago)
changeset 68853d36f00510e40
parent 68852 becaeaa334ae
child 68854 404e04f649d4
tuned signature;
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 30 14:10:39 2018 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 30 14:21:40 2018 +0200
     1.3 @@ -328,10 +328,10 @@
     1.4      |-> (fn (param_map, params, assm_axiom) =>
     1.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     1.6      #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
     1.7 -       Context.theory_map (Locale.add_registration
     1.8 +       Locale.add_registration_theory
     1.9           {dep = (class, base_morph),
    1.10             mixin = Option.map (rpair true) eq_morph,
    1.11 -           export = export_morph})
    1.12 +           export = export_morph}
    1.13      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    1.14      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    1.15      |> snd
     2.1 --- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:10:39 2018 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:21:40 2018 +0200
     2.3 @@ -370,7 +370,7 @@
     2.4    background_declaration decl #> standard_declaration (K true) decl;
     2.5  
     2.6  val theory_registration =
     2.7 -  Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
     2.8 +  Local_Theory.raw_theory o Locale.add_registration_theory;
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:10:39 2018 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:21:40 2018 +0200
     3.3 @@ -76,6 +76,7 @@
     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_theory: registration -> theory -> theory
     3.8    val add_registration_proof: registration -> Proof.context -> Proof.context
     3.9    val add_registration_local_theory: registration -> local_theory -> local_theory
    3.10    val activate_fragment: registration -> local_theory -> local_theory
    3.11 @@ -559,12 +560,13 @@
    3.12        |> activate_facts (SOME export) (name, morph)
    3.13    end;
    3.14  
    3.15 +val add_registration_theory = Context.theory_map o add_registration;
    3.16 +
    3.17  fun add_registration_proof registration ctxt = ctxt
    3.18    |> Proof_Context.set_stmt false
    3.19    |> Context.proof_map (add_registration registration)
    3.20    |> Proof_Context.restore_stmt ctxt;
    3.21  
    3.22 -
    3.23  fun add_registration_local_theory registration lthy =
    3.24    let val n = Local_Theory.level lthy in
    3.25      lthy |> Local_Theory.map_contexts (fn level =>
    3.26 @@ -607,8 +609,10 @@
    3.27      val (_, regs) =
    3.28        fold_rev (roundup thy' cons export)
    3.29          (registrations_of context' loc) (Idents.get context', []);
    3.30 -    fun add_dep dep = add_registration {dep = dep, mixin = NONE, export = export};
    3.31 -  in thy' |> fold_rev (Context.theory_map o add_dep) regs end;
    3.32 +  in
    3.33 +    thy'
    3.34 +    |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
    3.35 +  end;
    3.36  
    3.37  
    3.38  (*** Storing results ***)