tuned signature -- proper Local_Theory.add_thms_dynamic;

--- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 14:57:03 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 16:06:32 2014 +0200
@@ -59,6 +59,7 @@
   val subscription: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
+  val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
@@ -274,6 +275,20 @@
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
+fun add_thms_dynamic (binding, f) lthy =
+  lthy
+  |> background_theory_result (fn thy => thy
+      |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
+  |-> (fn name =>
+    map_contexts (fn _ => fn ctxt =>
+      Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
+    declaration {syntax = false, pervasive = false} (fn phi =>
+      let val binding' = Morphism.binding phi binding in
+        Context.mapping
+          (Global_Theory.alias_fact binding' name)
+          (Proof_Context.fact_alias binding' name)
+      end));
+
 fun set_defsort S =
   declaration {syntax = true, pervasive = false}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));

--- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 14:57:03 2014 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 16:06:32 2014 +0200
@@ -65,20 +65,10 @@
     val description =
       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     val lthy' = lthy
-      |> Local_Theory.background_theory
-        (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
-         Context.theory_map (new_entry name))
-      |> Local_Theory.map_contexts (fn _ => fn ctxt =>
-          ctxt
-          |> Context.proof_map (new_entry name)
-          |> Proof_Context.transfer_facts (Proof_Context.theory_of ctxt))
+      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
+      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
+      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
-      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
-          let val binding' = Morphism.binding phi binding in
-            Context.mapping
-              (Global_Theory.alias_fact binding' name)
-              (Proof_Context.fact_alias binding' name)
-          end);
   in (name, lthy') end;
 
 val _ =

--- a/src/Pure/global_theory.ML	Wed Aug 13 14:57:03 2014 +0200
+++ b/src/Pure/global_theory.ML	Wed Aug 13 16:06:32 2014 +0200
@@ -29,6 +29,8 @@
   val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
+  val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) ->
+    theory -> string * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     -> theory -> (string * thm list) list * theory
@@ -157,10 +159,14 @@
 val add_thm = yield_singleton add_thms;
 
 
-(* add_thms_dynamic *)
+(* dynamic theorems *)
 
-fun add_thms_dynamic (b, f) thy = thy
-  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
+fun add_thms_dynamic' context arg thy =
+  let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
+  in (name, Data.put facts' thy) end;
+
+fun add_thms_dynamic arg thy =
+  add_thms_dynamic' (Context.Theory thy) arg thy |> snd;
 
 
 (* note_thmss *)