tuned signature -- proper Local_Theory.add_thms_dynamic;
authorwenzelm
Wed Aug 13 16:06:32 2014 +0200 (2014-08-13)
changeset 57929c5063c033a5a
parent 57928 f4ff42c5b05b
child 57930 3b4deb99a932
tuned signature -- proper Local_Theory.add_thms_dynamic;
src/Pure/Isar/local_theory.ML
src/Pure/Tools/named_theorems.ML
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 14:57:03 2014 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 16:06:32 2014 +0200
     1.3 @@ -59,6 +59,7 @@
     1.4    val subscription: string * morphism -> (morphism * bool) option -> morphism ->
     1.5      local_theory -> local_theory
     1.6    val pretty: local_theory -> Pretty.T list
     1.7 +  val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
     1.8    val set_defsort: sort -> local_theory -> local_theory
     1.9    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    1.10    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.11 @@ -274,6 +275,20 @@
    1.12  val notes = notes_kind "";
    1.13  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    1.14  
    1.15 +fun add_thms_dynamic (binding, f) lthy =
    1.16 +  lthy
    1.17 +  |> background_theory_result (fn thy => thy
    1.18 +      |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
    1.19 +  |-> (fn name =>
    1.20 +    map_contexts (fn _ => fn ctxt =>
    1.21 +      Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
    1.22 +    declaration {syntax = false, pervasive = false} (fn phi =>
    1.23 +      let val binding' = Morphism.binding phi binding in
    1.24 +        Context.mapping
    1.25 +          (Global_Theory.alias_fact binding' name)
    1.26 +          (Proof_Context.fact_alias binding' name)
    1.27 +      end));
    1.28 +
    1.29  fun set_defsort S =
    1.30    declaration {syntax = true, pervasive = false}
    1.31      (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
     2.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 14:57:03 2014 +0200
     2.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 16:06:32 2014 +0200
     2.3 @@ -65,20 +65,10 @@
     2.4      val description =
     2.5        "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     2.6      val lthy' = lthy
     2.7 -      |> Local_Theory.background_theory
     2.8 -        (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
     2.9 -         Context.theory_map (new_entry name))
    2.10 -      |> Local_Theory.map_contexts (fn _ => fn ctxt =>
    2.11 -          ctxt
    2.12 -          |> Context.proof_map (new_entry name)
    2.13 -          |> Proof_Context.transfer_facts (Proof_Context.theory_of ctxt))
    2.14 +      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
    2.15 +      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
    2.16 +      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
    2.17        |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    2.18 -      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
    2.19 -          let val binding' = Morphism.binding phi binding in
    2.20 -            Context.mapping
    2.21 -              (Global_Theory.alias_fact binding' name)
    2.22 -              (Proof_Context.fact_alias binding' name)
    2.23 -          end);
    2.24    in (name, lthy') end;
    2.25  
    2.26  val _ =
     3.1 --- a/src/Pure/global_theory.ML	Wed Aug 13 14:57:03 2014 +0200
     3.2 +++ b/src/Pure/global_theory.ML	Wed Aug 13 16:06:32 2014 +0200
     3.3 @@ -29,6 +29,8 @@
     3.4    val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
     3.5    val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
     3.6    val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
     3.7 +  val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) ->
     3.8 +    theory -> string * theory
     3.9    val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
    3.10    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
    3.11      -> theory -> (string * thm list) list * theory
    3.12 @@ -157,10 +159,14 @@
    3.13  val add_thm = yield_singleton add_thms;
    3.14  
    3.15  
    3.16 -(* add_thms_dynamic *)
    3.17 +(* dynamic theorems *)
    3.18  
    3.19 -fun add_thms_dynamic (b, f) thy = thy
    3.20 -  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
    3.21 +fun add_thms_dynamic' context arg thy =
    3.22 +  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
    3.23 +  in (name, Data.put facts' thy) end;
    3.24 +
    3.25 +fun add_thms_dynamic arg thy =
    3.26 +  add_thms_dynamic' (Context.Theory thy) arg thy |> snd;
    3.27  
    3.28  
    3.29  (* note_thmss *)